Theorem pm5.17

Theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Jan-2013.)

Conclusion
\( \vdash (\varphi \vee \psi) \wedge \neg (\varphi \wedge \psi) \leftrightarrow (\varphi \leftrightarrow \neg \psi) \)
Proof
l0
bicom
\( \vdash \varphi \leftrightarrow \neg \psi \leftrightarrow (\neg \psi \leftrightarrow \varphi) \)
l1
dfbi2
\( \vdash \neg \psi \leftrightarrow \varphi \leftrightarrow (\neg \psi \rightarrow \varphi) \wedge (\varphi \rightarrow \neg \psi) \)
l2
orcom
\( \vdash \varphi \vee \psi \leftrightarrow \psi \vee \varphi \)
df-or
\( \vdash \psi \vee \varphi \leftrightarrow \neg \psi \rightarrow \varphi \)
l4
bitr2i l2 _
imnan
anbi12i l4 _
\( \vdash (\neg \psi \rightarrow \varphi) \wedge (\varphi \rightarrow \neg \psi) \leftrightarrow (\varphi \vee \psi) \wedge \neg (\varphi \wedge \psi) \)
3bitrri l0 l1 _