# Metamath Proof Explorer

## Theorem dfbi1

Description: Relate the biconditional connective to primitive connectives. See dfbi1ALT for an unusual version proved directly from axioms. (Contributed by NM, 29-Dec-1992)

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