Metamath Proof Explorer

Theorem bj-nnfor

Description: Nonfreeness in both disjuncts implies nonfreeness in the disjunction. (Contributed by BJ, 19-Nov-2023) In classical logic, there is a proof using the definition of disjunction in terms of implication and negation, so using bj-nnfim , bj-nnfnt and bj-nnfbi , but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)

Ref Expression
Assertion bj-nnfor 
|- ( ( F// x ph /\ F// x ps ) -> F// x ( ph \/ ps ) )

Proof

Step Hyp Ref Expression
1 df-bj-nnf 
 |-  ( F// x ph <-> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) )
2 df-bj-nnf 
 |-  ( F// x ps <-> ( ( E. x ps -> ps ) /\ ( ps -> A. x ps ) ) )
3 19.43 
 |-  ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) )
4 pm3.48 
 |-  ( ( ( E. x ph -> ph ) /\ ( E. x ps -> ps ) ) -> ( ( E. x ph \/ E. x ps ) -> ( ph \/ ps ) ) )
5 3 4 syl5bi 
 |-  ( ( ( E. x ph -> ph ) /\ ( E. x ps -> ps ) ) -> ( E. x ( ph \/ ps ) -> ( ph \/ ps ) ) )
6 pm3.48 
 |-  ( ( ( ph -> A. x ph ) /\ ( ps -> A. x ps ) ) -> ( ( ph \/ ps ) -> ( A. x ph \/ A. x ps ) ) )
7 19.33 
 |-  ( ( A. x ph \/ A. x ps ) -> A. x ( ph \/ ps ) )
8 6 7 syl6 
 |-  ( ( ( ph -> A. x ph ) /\ ( ps -> A. x ps ) ) -> ( ( ph \/ ps ) -> A. x ( ph \/ ps ) ) )
9 5 8 anim12i 
 |-  ( ( ( ( E. x ph -> ph ) /\ ( E. x ps -> ps ) ) /\ ( ( ph -> A. x ph ) /\ ( ps -> A. x ps ) ) ) -> ( ( E. x ( ph \/ ps ) -> ( ph \/ ps ) ) /\ ( ( ph \/ ps ) -> A. x ( ph \/ ps ) ) ) )
10 9 an4s 
 |-  ( ( ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) /\ ( ( E. x ps -> ps ) /\ ( ps -> A. x ps ) ) ) -> ( ( E. x ( ph \/ ps ) -> ( ph \/ ps ) ) /\ ( ( ph \/ ps ) -> A. x ( ph \/ ps ) ) ) )
11 1 2 10 syl2anb 
 |-  ( ( F// x ph /\ F// x ps ) -> ( ( E. x ( ph \/ ps ) -> ( ph \/ ps ) ) /\ ( ( ph \/ ps ) -> A. x ( ph \/ ps ) ) ) )
12 df-bj-nnf 
 |-  ( F// x ( ph \/ ps ) <-> ( ( E. x ( ph \/ ps ) -> ( ph \/ ps ) ) /\ ( ( ph \/ ps ) -> A. x ( ph \/ ps ) ) ) )
13 11 12 sylibr 
 |-  ( ( F// x ph /\ F// x ps ) -> F// x ( ph \/ ps ) )