Theorem xorcom

The connector \/_ is commutative. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 21-Apr-2024.)

Conclusion
\( \vdash \varphi \veebar \psi \leftrightarrow \psi \veebar \varphi \)
Proof
l0
df-xor
\( \vdash \varphi \veebar \psi \leftrightarrow \neg (\varphi \leftrightarrow \psi) \)
bicom
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\psi \leftrightarrow \varphi) \)
l2
xchbinx l0 _
\( \vdash \varphi \veebar \psi \leftrightarrow \neg (\psi \leftrightarrow \varphi) \)
df-xor
\( \vdash \psi \veebar \varphi \leftrightarrow \neg (\psi \leftrightarrow \varphi) \)
bitr4i l2 _