This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-nnford

Description: Nonfreeness in both disjuncts implies nonfreeness in the disjunction, deduction form. See comments for bj-nnfor and bj-nnfand . (Contributed by BJ, 2-Dec-2023) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-nnford.1 
|- ( ph -> F// x ps )
bj-nnford.2 
|- ( ph -> F// x ch )
Assertion bj-nnford 
|- ( ph -> F// x ( ps \/ ch ) )

Proof

Step Hyp Ref Expression
1 bj-nnford.1 
 |-  ( ph -> F// x ps )
2 bj-nnford.2 
 |-  ( ph -> F// x ch )
3 19.43 
 |-  ( E. x ( ps \/ ch ) <-> ( E. x ps \/ E. x ch ) )
4 1 bj-nnfed 
 |-  ( ph -> ( E. x ps -> ps ) )
5 2 bj-nnfed 
 |-  ( ph -> ( E. x ch -> ch ) )
6 4 5 orim12d 
 |-  ( ph -> ( ( E. x ps \/ E. x ch ) -> ( ps \/ ch ) ) )
7 3 6 biimtrid 
 |-  ( ph -> ( E. x ( ps \/ ch ) -> ( ps \/ ch ) ) )
8 1 bj-nnfad 
 |-  ( ph -> ( ps -> A. x ps ) )
9 2 bj-nnfad 
 |-  ( ph -> ( ch -> A. x ch ) )
10 8 9 orim12d 
 |-  ( ph -> ( ( ps \/ ch ) -> ( A. x ps \/ A. x ch ) ) )
11 19.33 
 |-  ( ( A. x ps \/ A. x ch ) -> A. x ( ps \/ ch ) )
12 10 11 syl6 
 |-  ( ph -> ( ( ps \/ ch ) -> A. x ( ps \/ ch ) ) )
13 df-bj-nnf 
 |-  ( F// x ( ps \/ ch ) <-> ( ( E. x ( ps \/ ch ) -> ( ps \/ ch ) ) /\ ( ( ps \/ ch ) -> A. x ( ps \/ ch ) ) ) )
14 7 12 13 sylanbrc 
 |-  ( ph -> F// x ( ps \/ ch ) )