Metamath Proof Explorer

Theorem bj-nnfand

Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan , it has two more essential steps but fewer total steps (since there are fewer intermediate formulas to build) and is easier to follow and understand. This statement is of intermediate complexity: for simpler statements, closed-style proofs like that of bj-nnfan will generally be shorter than deduction-style proofs while still easy to follow, while for more complex statements, the opposite will be true (and deduction-style proofs like that of bj-nnfand will generally be easier to understand). (Contributed by BJ, 19-Nov-2023) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-nnfand.1 ⊢ φ → Ⅎ' x ψ
bj-nnfand.2 ⊢ φ → Ⅎ' x χ
Assertion bj-nnfand ⊢ φ → Ⅎ' x ψ ∧ χ

Proof

Step Hyp Ref Expression
1 bj-nnfand.1 ⊢ φ → Ⅎ' x ψ
2 bj-nnfand.2 ⊢ φ → Ⅎ' x χ
3 19.40 ⊢ ∃ x ψ ∧ χ → ∃ x ψ ∧ ∃ x χ
4 1 bj-nnfed ⊢ φ → ∃ x ψ → ψ
5 2 bj-nnfed ⊢ φ → ∃ x χ → χ
6 4 5 anim12d ⊢ φ → ∃ x ψ ∧ ∃ x χ → ψ ∧ χ
7 3 6 syl5 ⊢ φ → ∃ x ψ ∧ χ → ψ ∧ χ
8 1 bj-nnfad ⊢ φ → ψ → ∀ x ψ
9 2 bj-nnfad ⊢ φ → χ → ∀ x χ
10 8 9 anim12d ⊢ φ → ψ ∧ χ → ∀ x ψ ∧ ∀ x χ
11 19.26 ⊢ ∀ x ψ ∧ χ ↔ ∀ x ψ ∧ ∀ x χ
12 10 11 imbitrrdi ⊢ φ → ψ ∧ χ → ∀ x ψ ∧ χ
13 df-bj-nnf ⊢ Ⅎ' x ψ ∧ χ ↔ ∃ x ψ ∧ χ → ψ ∧ χ ∧ ψ ∧ χ → ∀ x ψ ∧ χ
14 7 12 13 sylanbrc ⊢ φ → Ⅎ' x ψ ∧ χ