Metamath Proof Explorer

Theorem biimp

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

Ref Expression
Assertion biimp ${⊢}\left({\phi }↔{\psi }\right)\to \left({\phi }\to {\psi }\right)$

Proof

Step Hyp Ref Expression
1 df-bi ${⊢}¬\left(\left(\left({\phi }↔{\psi }\right)\to ¬\left(\left({\phi }\to {\psi }\right)\to ¬\left({\psi }\to {\phi }\right)\right)\right)\to ¬\left(¬\left(\left({\phi }\to {\psi }\right)\to ¬\left({\psi }\to {\phi }\right)\right)\to \left({\phi }↔{\psi }\right)\right)\right)$
2 simplim ${⊢}¬\left(\left(\left({\phi }↔{\psi }\right)\to ¬\left(\left({\phi }\to {\psi }\right)\to ¬\left({\psi }\to {\phi }\right)\right)\right)\to ¬\left(¬\left(\left({\phi }\to {\psi }\right)\to ¬\left({\psi }\to {\phi }\right)\right)\to \left({\phi }↔{\psi }\right)\right)\right)\to \left(\left({\phi }↔{\psi }\right)\to ¬\left(\left({\phi }\to {\psi }\right)\to ¬\left({\psi }\to {\phi }\right)\right)\right)$
3 1 2 ax-mp ${⊢}\left({\phi }↔{\psi }\right)\to ¬\left(\left({\phi }\to {\psi }\right)\to ¬\left({\psi }\to {\phi }\right)\right)$
4 simplim ${⊢}¬\left(\left({\phi }\to {\psi }\right)\to ¬\left({\psi }\to {\phi }\right)\right)\to \left({\phi }\to {\psi }\right)$
5 3 4 syl ${⊢}\left({\phi }↔{\psi }\right)\to \left({\phi }\to {\psi }\right)$