Theorem pm5.24

Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)

Conclusion
\( \vdash \neg (\varphi \wedge \psi \vee \neg \varphi \wedge \neg \psi) \leftrightarrow \varphi \wedge \neg \psi \vee \psi \wedge \neg \varphi \)
Proof
l0
xor
\( \vdash \neg (\varphi \leftrightarrow \psi) \leftrightarrow \varphi \wedge \neg \psi \vee \psi \wedge \neg \varphi \)
dfbi3
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \neg \psi \)
xchnxbi l0 _