Definition [df-bi] rewritten in an abbreviated form to help intuitive
understanding of that definition. Note that it is a conjunction of two
implications; one which asserts properties that follow from the
biconditional and one which asserts properties that imply the
biconditional. (Contributed by NM, 15-Aug-2008.)
\( \vdash ((\varphi \leftrightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)) \wedge ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \rightarrow (\varphi \leftrightarrow \psi)) \)
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \)
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \leftrightarrow ((\varphi \leftrightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)) \wedge ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \rightarrow (\varphi \leftrightarrow \psi)) \)