Metamath Proof Explorer

Theorem bj-nnfbid

Description: Nonfreeness in both sides implies nonfreeness in the biconditional, deduction form. (Contributed by BJ, 2-Dec-2023) (Proof modification is discouraged.)

		Ref	Expression
	Hypotheses	bj-nnfbid.1	$⊢ φ \to Ⅎ' x ψ$
		bj-nnfbid.2	$⊢ φ \to Ⅎ' x χ$
	Assertion	bj-nnfbid	$⊢ φ \to Ⅎ' x (ψ \leftrightarrow χ)$

Proof

Step	Hyp	Ref	Expression
1		bj-nnfbid.1	$⊢ φ \to Ⅎ' x ψ$
2		bj-nnfbid.2	$⊢ φ \to Ⅎ' x χ$
3		bj-nnfim	$⊢ (Ⅎ' x ψ \land Ⅎ' x χ) \to Ⅎ' x (ψ \to χ)$
4	1 2 3	syl2anc	$⊢ φ \to Ⅎ' x (ψ \to χ)$
5		bj-nnfim	$⊢ (Ⅎ' x χ \land Ⅎ' x ψ) \to Ⅎ' x (χ \to ψ)$
6	2 1 5	syl2anc	$⊢ φ \to Ⅎ' x (χ \to ψ)$
7	4 6	bj-nnfand	$⊢ φ \to Ⅎ' x ((ψ \to χ) \land (χ \to ψ))$
8		dfbi2	$⊢ (ψ \leftrightarrow χ) \leftrightarrow ((ψ \to χ) \land (χ \to ψ))$
9	8	bj-nnfbii	$⊢ Ⅎ' x (ψ \leftrightarrow χ) \leftrightarrow Ⅎ' x ((ψ \to χ) \land (χ \to ψ))$
10	7 9	sylibr	$⊢ φ \to Ⅎ' x (ψ \leftrightarrow χ)$