# Metamath Proof Explorer

## Theorem impbi

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

Ref Expression
Assertion impbi ${⊢}\left({\phi }\to {\psi }\right)\to \left(\left({\psi }\to {\phi }\right)\to \left({\phi }↔{\psi }\right)\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 simprim ${⊢}¬\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(\left({\phi }\to {\psi }\right)\to ¬\left({\psi }\to {\phi }\right)\right)\to \left({\phi }↔{\psi }\right)\right)$
3 1 2 ax-mp ${⊢}¬\left(\left({\phi }\to {\psi }\right)\to ¬\left({\psi }\to {\phi }\right)\right)\to \left({\phi }↔{\psi }\right)$
4 3 expi ${⊢}\left({\phi }\to {\psi }\right)\to \left(\left({\psi }\to {\phi }\right)\to \left({\phi }↔{\psi }\right)\right)$