Theorem dfbi2

A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 24-Jan-1993.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \)
Proof
l0
dfbi1
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \)
df-an
\( \vdash (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \leftrightarrow \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \)
bitr4i l0 _