frege54cor0a

Description: Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	frege54cor0a	$⊢ (ψ \leftrightarrow φ) \leftrightarrow if- (ψ, φ, \neg φ)$

Step	Hyp	Ref	Expression
1		ax-frege28	$⊢ (φ \to ψ) \to (\neg ψ \to \neg φ)$
2	1	anim2i	$⊢ ((ψ \to φ) \land (φ \to ψ)) \to ((ψ \to φ) \land (\neg ψ \to \neg φ))$
3		con4	$⊢ (\neg ψ \to \neg φ) \to (φ \to ψ)$
4	3	anim2i	$⊢ ((ψ \to φ) \land (\neg ψ \to \neg φ)) \to ((ψ \to φ) \land (φ \to ψ))$
5	2 4	impbii	$⊢ ((ψ \to φ) \land (φ \to ψ)) \leftrightarrow ((ψ \to φ) \land (\neg ψ \to \neg φ))$
6		dfbi2	$⊢ (ψ \leftrightarrow φ) \leftrightarrow ((ψ \to φ) \land (φ \to ψ))$
7		dfifp2	$⊢ if- (ψ, φ, \neg φ) \leftrightarrow ((ψ \to φ) \land (\neg ψ \to \neg φ))$
8	5 6 7	3bitr4i	$⊢ (ψ \leftrightarrow φ) \leftrightarrow if- (ψ, φ, \neg φ)$

Metamath Proof Explorer