Metamath Proof Explorer

Theorem bj-nnfbit

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

		Ref	Expression
	Assertion	bj-nnfbit	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to Ⅎ' x (φ \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		bj-nnfim	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to Ⅎ' x (φ \to ψ)$
2		bj-nnfim	$⊢ (Ⅎ' x ψ \land Ⅎ' x φ) \to Ⅎ' x (ψ \to φ)$
3	2	ancoms	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to Ⅎ' x (ψ \to φ)$
4		bj-nnfan	$⊢ (Ⅎ' x (φ \to ψ) \land Ⅎ' x (ψ \to φ)) \to Ⅎ' x ((φ \to ψ) \land (ψ \to φ))$
5	1 3 4	syl2anc	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to Ⅎ' x ((φ \to ψ) \land (ψ \to φ))$
6		dfbi2	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$
7	6	bicomi	$⊢ ((φ \to ψ) \land (ψ \to φ)) \leftrightarrow (φ \leftrightarrow ψ)$
8	7	bj-nnfbii	$⊢ Ⅎ' x ((φ \to ψ) \land (ψ \to φ)) \leftrightarrow Ⅎ' x (φ \leftrightarrow ψ)$
9	5 8	sylib	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to Ⅎ' x (φ \leftrightarrow ψ)$