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 ( 𝜑 → Ⅎ' 𝑥 𝜓 )
bj-nnfand.2 ( 𝜑 → Ⅎ' 𝑥 𝜒 )
Assertion bj-nnfand ( 𝜑 → Ⅎ' 𝑥 ( 𝜓𝜒 ) )

Proof

Step Hyp Ref Expression
1 bj-nnfand.1 ( 𝜑 → Ⅎ' 𝑥 𝜓 )
2 bj-nnfand.2 ( 𝜑 → Ⅎ' 𝑥 𝜒 )
3 19.40 ( ∃ 𝑥 ( 𝜓𝜒 ) → ( ∃ 𝑥 𝜓 ∧ ∃ 𝑥 𝜒 ) )
4 1 bj-nnfed ( 𝜑 → ( ∃ 𝑥 𝜓𝜓 ) )
5 2 bj-nnfed ( 𝜑 → ( ∃ 𝑥 𝜒𝜒 ) )
6 4 5 anim12d ( 𝜑 → ( ( ∃ 𝑥 𝜓 ∧ ∃ 𝑥 𝜒 ) → ( 𝜓𝜒 ) ) )
7 3 6 syl5 ( 𝜑 → ( ∃ 𝑥 ( 𝜓𝜒 ) → ( 𝜓𝜒 ) ) )
8 1 bj-nnfad ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜓 ) )
9 2 bj-nnfad ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜒 ) )
10 8 9 anim12d ( 𝜑 → ( ( 𝜓𝜒 ) → ( ∀ 𝑥 𝜓 ∧ ∀ 𝑥 𝜒 ) ) )
11 19.26 ( ∀ 𝑥 ( 𝜓𝜒 ) ↔ ( ∀ 𝑥 𝜓 ∧ ∀ 𝑥 𝜒 ) )
12 10 11 syl6ibr ( 𝜑 → ( ( 𝜓𝜒 ) → ∀ 𝑥 ( 𝜓𝜒 ) ) )
13 df-bj-nnf ( Ⅎ' 𝑥 ( 𝜓𝜒 ) ↔ ( ( ∃ 𝑥 ( 𝜓𝜒 ) → ( 𝜓𝜒 ) ) ∧ ( ( 𝜓𝜒 ) → ∀ 𝑥 ( 𝜓𝜒 ) ) ) )
14 7 12 13 sylanbrc ( 𝜑 → Ⅎ' 𝑥 ( 𝜓𝜒 ) )