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 ⊢Ⅎ'xφ∧Ⅎ'xψ→Ⅎ'xφ∨ψ

Proof

Step Hyp Ref Expression
1 df-bj-nnf ⊢Ⅎ'xφ↔∃xφ→φ∧φ→∀xφ
2 df-bj-nnf ⊢Ⅎ'xψ↔∃xψ→ψ∧ψ→∀xψ
3 19.43 ⊢∃xφ∨ψ↔∃xφ∨∃xψ
4 pm3.48 ⊢∃xφ→φ∧∃xψ→ψ→∃xφ∨∃xψ→φ∨ψ
5 3 4 biimtrid ⊢∃xφ→φ∧∃xψ→ψ→∃xφ∨ψ→φ∨ψ
6 pm3.48 ⊢φ→∀xφ∧ψ→∀xψ→φ∨ψ→∀xφ∨∀xψ
7 19.33 ⊢∀xφ∨∀xψ→∀xφ∨ψ
8 6 7 syl6 ⊢φ→∀xφ∧ψ→∀xψ→φ∨ψ→∀xφ∨ψ
9 5 8 anim12i ⊢∃xφ→φ∧∃xψ→ψ∧φ→∀xφ∧ψ→∀xψ→∃xφ∨ψ→φ∨ψ∧φ∨ψ→∀xφ∨ψ
10 9 an4s ⊢∃xφ→φ∧φ→∀xφ∧∃xψ→ψ∧ψ→∀xψ→∃xφ∨ψ→φ∨ψ∧φ∨ψ→∀xφ∨ψ
11 1 2 10 syl2anb ⊢Ⅎ'xφ∧Ⅎ'xψ→∃xφ∨ψ→φ∨ψ∧φ∨ψ→∀xφ∨ψ
12 df-bj-nnf ⊢Ⅎ'xφ∨ψ↔∃xφ∨ψ→φ∨ψ∧φ∨ψ→∀xφ∨ψ
13 11 12 sylibr ⊢Ⅎ'xφ∧Ⅎ'xψ→Ⅎ'xφ∨ψ