Metamath Proof Explorer

Theorem biimpexp

Description: A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010)

		Ref	Expression
	Assertion	biimpexp	$⊢ ((φ \leftrightarrow ψ) \to χ) \leftrightarrow ((φ \to ψ) \to ((ψ \to φ) \to χ))$

Step	Hyp	Ref	Expression
1		dfbi2	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$
2	1	imbi1i	$⊢ ((φ \leftrightarrow ψ) \to χ) \leftrightarrow (((φ \to ψ) \land (ψ \to φ)) \to χ)$
3		impexp	$⊢ (((φ \to ψ) \land (ψ \to φ)) \to χ) \leftrightarrow ((φ \to ψ) \to ((ψ \to φ) \to χ))$
4	2 3	bitri	$⊢ ((φ \leftrightarrow ψ) \to χ) \leftrightarrow ((φ \to ψ) \to ((ψ \to φ) \to χ))$