Theorem dfbi3

An alternate definition of the biconditional. Theorem *5.23 of [WhiteheadRussell] p. 124. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) (Proof shortened by NM, 29-Oct-2021.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \neg \psi \)
Proof
con34b
l1
anbi2i _
\( \vdash (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \neg \psi) \)
l2
dfbi2
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \)
cases2
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \neg \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \neg \psi) \)
3bitr4i l1 l2 _