Theorem pm5.18

Theorem *5.18 of [WhiteheadRussell] p. 124. This theorem says that logical equivalence is the same as negated "exclusive or". (Contributed by NM, 28-Jun-2002.) (Proof shortened by Andrew Salmon, 20-Jun-2011.) (Proof shortened by Wolf Lammen, 15-Oct-2013.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \neg (\varphi \leftrightarrow \neg \psi) \)
Proof
pm5.501
l1
con1bid _
\( \vdash \varphi \rightarrow (\neg (\varphi \leftrightarrow \neg \psi) \leftrightarrow \psi) \)
pm5.501
\( \vdash \varphi \rightarrow (\psi \leftrightarrow (\varphi \leftrightarrow \psi)) \)
l3
bitr2d l1 _
\( \vdash \varphi \rightarrow (\varphi \leftrightarrow \psi \leftrightarrow \neg (\varphi \leftrightarrow \neg \psi)) \)
nbn2
l5
con1bid _
\( \vdash \neg \varphi \rightarrow (\neg (\varphi \leftrightarrow \neg \psi) \leftrightarrow \neg \psi) \)
nbn2
\( \vdash \neg \varphi \rightarrow (\neg \psi \leftrightarrow (\varphi \leftrightarrow \psi)) \)
bitr2d l5 _
\( \vdash \neg \varphi \rightarrow (\varphi \leftrightarrow \psi \leftrightarrow \neg (\varphi \leftrightarrow \neg \psi)) \)
pm2.61i l3 _