biimp

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

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

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		simplim	$⊢ \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ)))$
3	1 2	ax-mp	$⊢ (φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))$
4		simplim	$⊢ \neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \to ψ)$
5	3 4	syl	$⊢ (φ \leftrightarrow ψ) \to (φ \to ψ)$

Metamath Proof Explorer