Theorem dfbi1

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

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \)
Proof
l0
df-bi
\( \vdash \neg (((\varphi \leftrightarrow \psi) \rightarrow \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi))) \rightarrow \neg (\neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \rightarrow (\varphi \leftrightarrow \psi))) \)
impbi
con3rr3 _
\( \vdash \neg (\varphi \leftrightarrow \psi \leftrightarrow \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi))) \rightarrow ((\varphi \leftrightarrow \psi) \rightarrow \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi))) \rightarrow \neg (\neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \rightarrow (\varphi \leftrightarrow \psi)) \)
mt3 l0 _