Theorem xor

Two ways to express exclusive disjunction ( [df-xor] ). Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.)

Conclusion
\( \vdash \neg (\varphi \leftrightarrow \psi) \leftrightarrow \varphi \wedge \neg \psi \vee \psi \wedge \neg \varphi \)
Proof
l0
iman
iman
l2
anbi12i l0 _
\( \vdash (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \leftrightarrow \neg (\varphi \wedge \neg \psi) \wedge \neg (\psi \wedge \neg \varphi) \)
l3
dfbi2
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \)
ioran
\( \vdash \neg (\varphi \wedge \neg \psi \vee \psi \wedge \neg \varphi) \leftrightarrow \neg (\varphi \wedge \neg \psi) \wedge \neg (\psi \wedge \neg \varphi) \)
3bitr4ri l2 l3 _
con1bii _