Conjunction distributes over exclusive-or, using \( \neg (\varphi \leftrightarrow \psi) \) to
express exclusive-or. This is one way to interpret the distributive law
of multiplication over addition in modulo 2 arithmetic. This is not
necessarily true in intuitionistic logic, though anxordi does hold in
it. (Contributed by NM, 3-Oct-2008.)
\( \vdash \varphi \wedge \neg (\psi \leftrightarrow \chi) \leftrightarrow \neg (\varphi \wedge \psi \leftrightarrow \varphi \wedge \chi) \)
\( \vdash \varphi \wedge \neg (\psi \leftrightarrow \chi) \leftrightarrow \neg (\varphi \rightarrow (\psi \leftrightarrow \chi)) \)
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \leftrightarrow (\varphi \wedge \psi \leftrightarrow \varphi \wedge \chi) \)