Theorem xorass
The connector \/_ is associative. (Contributed by FL, 22-Nov-2010.)
(Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Wolf
Lammen, 20-Jun-2020.)
Conclusion
\( \vdash (\varphi \veebar \psi) \veebar \chi \leftrightarrow \varphi \veebar (\psi \veebar \chi) \)
Proof
l0
xor3
\( \vdash \neg (\varphi \leftrightarrow \psi \veebar \chi) \leftrightarrow (\varphi \leftrightarrow \neg (\psi \veebar \chi)) \)
l1
biass
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow (\varphi \leftrightarrow (\psi \leftrightarrow \chi)) \)
xnor
l3
bibi1i _
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \chi \leftrightarrow (\neg (\varphi \veebar \psi) \leftrightarrow \chi) \)
xnor
bibi2i _
\( \vdash \varphi \leftrightarrow (\psi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow \neg (\psi \veebar \chi)) \)
l6
3bitr3i l1 l3 _
\( \vdash \neg (\varphi \veebar \psi) \leftrightarrow \chi \leftrightarrow (\varphi \leftrightarrow \neg (\psi \veebar \chi)) \)
nbbn
\( \vdash \neg (\varphi \veebar \psi) \leftrightarrow \chi \leftrightarrow \neg (\varphi \veebar \psi \leftrightarrow \chi) \)
l8
3bitr2ri l0 l6 _
\( \vdash \neg (\varphi \veebar \psi \leftrightarrow \chi) \leftrightarrow \neg (\varphi \leftrightarrow \psi \veebar \chi) \)
l9
df-xor
\( \vdash (\varphi \veebar \psi) \veebar \chi \leftrightarrow \neg (\varphi \veebar \psi \leftrightarrow \chi) \)
df-xor
\( \vdash \varphi \veebar (\psi \veebar \chi) \leftrightarrow \neg (\varphi \leftrightarrow \psi \veebar \chi) \)
3bitr4i l8 l9 _