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	imbitrrdi	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → ∀ 𝑥 ( 𝜓 ∧ 𝜒 ) ) )
13		df-bj-nnf	⊢ ( Ⅎ' 𝑥 ( 𝜓 ∧ 𝜒 ) ↔ ( ( ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜒 ) ) ∧ ( ( 𝜓 ∧ 𝜒 ) → ∀ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) )
14	7 12 13	sylanbrc	⊢ ( 𝜑 → Ⅎ' 𝑥 ( 𝜓 ∧ 𝜒 ) )

Metamath Proof Explorer

Theorem bj-nnfand

Proof