impbi

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999)

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

Step	Hyp	Ref	Expression
1		df-bi	$⊢ \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))$
2		simprim	$⊢ \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))$
3	1 2	ax-mp	$⊢ \neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)$
4	3	expi	$⊢ (φ \to ψ) \to ((ψ \to φ) \to (φ \leftrightarrow ψ))$

Metamath Proof Explorer