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 ⊢ φ → Ⅎ' x ψ
bj-nnford.2 ⊢ φ → Ⅎ' x χ
Assertion bj-nnford ⊢ φ → Ⅎ' x ψ ∨ χ

Proof

Step Hyp Ref Expression
1 bj-nnford.1 ⊢ φ → Ⅎ' x ψ
2 bj-nnford.2 ⊢ φ → Ⅎ' x χ
3 19.43 ⊢ ∃ x ψ ∨ χ ↔ ∃ x ψ ∨ ∃ x χ
4 1 bj-nnfed ⊢ φ → ∃ x ψ → ψ
5 2 bj-nnfed ⊢ φ → ∃ x χ → χ
6 4 5 orim12d ⊢ φ → ∃ x ψ ∨ ∃ x χ → ψ ∨ χ
7 3 6 biimtrid ⊢ φ → ∃ x ψ ∨ χ → ψ ∨ χ
8 1 bj-nnfad ⊢ φ → ψ → ∀ x ψ
9 2 bj-nnfad ⊢ φ → χ → ∀ x χ
10 8 9 orim12d ⊢ φ → ψ ∨ χ → ∀ x ψ ∨ ∀ x χ
11 19.33 ⊢ ∀ x ψ ∨ ∀ x χ → ∀ x ψ ∨ χ
12 10 11 syl6 ⊢ φ → ψ ∨ χ → ∀ x ψ ∨ χ
13 df-bj-nnf ⊢ Ⅎ' x ψ ∨ χ ↔ ∃ x ψ ∨ χ → ψ ∨ χ ∧ ψ ∨ χ → ∀ x ψ ∨ χ
14 7 12 13 sylanbrc ⊢ φ → Ⅎ' x ψ ∨ χ