Theorem anxordi

Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi does not necessarily hold, in part because the usual definition of xor is subtly different in intuitionistic logic. (Contributed by David A. Wheeler, 7-Oct-2018.)

Conclusion
\( \vdash \varphi \wedge (\psi \veebar \chi) \leftrightarrow \varphi \wedge \psi \veebar \varphi \wedge \chi \)
Proof
l0
xordi
\( \vdash \varphi \wedge \neg (\psi \leftrightarrow \chi) \leftrightarrow \neg (\varphi \wedge \psi \leftrightarrow \varphi \wedge \chi) \)
df-xor
l2
anbi2i _
\( \vdash \varphi \wedge (\psi \veebar \chi) \leftrightarrow \varphi \wedge \neg (\psi \leftrightarrow \chi) \)
df-xor
\( \vdash \varphi \wedge \psi \veebar \varphi \wedge \chi \leftrightarrow \neg (\varphi \wedge \psi \leftrightarrow \varphi \wedge \chi) \)
3bitr4i l0 l2 _