dfbi

Description: Definition df-bi rewritten in an abbreviated form to help intuitive understanding of that definition. Note that it is a conjunction of two implications; one which asserts properties that follow from the biconditional and one which asserts properties that imply the biconditional. (Contributed by NM, 15-Aug-2008)

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

Proof

Step	Hyp	Ref	Expression
1		dfbi2	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$
2		dfbi2	$⊢ ((φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))) \leftrightarrow (((φ \leftrightarrow ψ) \to ((φ \to ψ) \land (ψ \to φ))) \land (((φ \to ψ) \land (ψ \to φ)) \to (φ \leftrightarrow ψ)))$
3	1 2	mpbi	$⊢ (((φ \leftrightarrow ψ) \to ((φ \to ψ) \land (ψ \to φ))) \land (((φ \to ψ) \land (ψ \to φ)) \to (φ \leftrightarrow ψ)))$

Metamath Proof Explorer

Theorem dfbi

Proof