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

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 φ ∨ ψ