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	$⊢ φ \to Ⅎ' x ψ$
	bj-nnfand.2	$⊢ φ \to Ⅎ' x χ$
Assertion	bj-nnfand	$⊢ φ \to Ⅎ' x (ψ \land χ)$

Proof

Step	Hyp	Ref	Expression
1		bj-nnfand.1	$⊢ φ \to Ⅎ' x ψ$
2		bj-nnfand.2	$⊢ φ \to Ⅎ' x χ$
3		19.40	$⊢ \exists x (ψ \land χ) \to (\exists x ψ \land \exists x χ)$
4	1	bj-nnfed	$⊢ φ \to (\exists x ψ \to ψ)$
5	2	bj-nnfed	$⊢ φ \to (\exists x χ \to χ)$
6	4 5	anim12d	$⊢ φ \to ((\exists x ψ \land \exists x χ) \to (ψ \land χ))$
7	3 6	syl5	$⊢ φ \to (\exists x (ψ \land χ) \to (ψ \land χ))$
8	1	bj-nnfad	$⊢ φ \to (ψ \to \forall x ψ)$
9	2	bj-nnfad	$⊢ φ \to (χ \to \forall x χ)$
10	8 9	anim12d	$⊢ φ \to ((ψ \land χ) \to (\forall x ψ \land \forall x χ))$
11		19.26	$⊢ \forall x (ψ \land χ) \leftrightarrow (\forall x ψ \land \forall x χ)$
12	10 11	imbitrrdi	$⊢ φ \to ((ψ \land χ) \to \forall x (ψ \land χ))$
13		df-bj-nnf	$⊢ Ⅎ' x (ψ \land χ) \leftrightarrow ((\exists x (ψ \land χ) \to (ψ \land χ)) \land ((ψ \land χ) \to \forall x (ψ \land χ)))$
14	7 12 13	sylanbrc	$⊢ φ \to Ⅎ' x (ψ \land χ)$

Metamath Proof Explorer

Theorem bj-nnfand

Proof