Metamath Proof Explorer

Theorem dfbi2

Description: A theorem similar to the standard definition of the biconditional. Definition of Margaris p. 49. (Contributed by NM, 24-Jan-1993)

		Ref	Expression
	Assertion	dfbi2	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$

Step	Hyp	Ref	Expression
1		dfbi1	$⊢ (φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))$
2		df-an	$⊢ ((φ \to ψ) \land (ψ \to φ)) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))$
3	1 2	bitr4i	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$