Theorem xorass

Description: 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)

	Ref	Expression
Assertion	xorass	⊢ ( ( ( 𝜑 ⊻ 𝜓 ) ⊻ 𝜒 ) ↔ ( 𝜑 ⊻ ( 𝜓 ⊻ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xor3	⊢ ( ¬ ( 𝜑 ↔ ( 𝜓 ⊻ 𝜒 ) ) ↔ ( 𝜑 ↔ ¬ ( 𝜓 ⊻ 𝜒 ) ) )
2		biass	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ↔ 𝜒 ) ↔ ( 𝜑 ↔ ( 𝜓 ↔ 𝜒 ) ) )
3		xnor	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( 𝜑 ⊻ 𝜓 ) )
4	3	bibi1i	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ↔ 𝜒 ) ↔ ( ¬ ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) )
5		xnor	⊢ ( ( 𝜓 ↔ 𝜒 ) ↔ ¬ ( 𝜓 ⊻ 𝜒 ) )
6	5	bibi2i	⊢ ( ( 𝜑 ↔ ( 𝜓 ↔ 𝜒 ) ) ↔ ( 𝜑 ↔ ¬ ( 𝜓 ⊻ 𝜒 ) ) )
7	2 4 6	3bitr3i	⊢ ( ( ¬ ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) ↔ ( 𝜑 ↔ ¬ ( 𝜓 ⊻ 𝜒 ) ) )
8		nbbn	⊢ ( ( ¬ ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) ↔ ¬ ( ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) )
9	1 7 8	3bitr2ri	⊢ ( ¬ ( ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) ↔ ¬ ( 𝜑 ↔ ( 𝜓 ⊻ 𝜒 ) ) )
10		df-xor	⊢ ( ( ( 𝜑 ⊻ 𝜓 ) ⊻ 𝜒 ) ↔ ¬ ( ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) )
11		df-xor	⊢ ( ( 𝜑 ⊻ ( 𝜓 ⊻ 𝜒 ) ) ↔ ¬ ( 𝜑 ↔ ( 𝜓 ⊻ 𝜒 ) ) )
12	9 10 11	3bitr4i	⊢ ( ( ( 𝜑 ⊻ 𝜓 ) ⊻ 𝜒 ) ↔ ( 𝜑 ⊻ ( 𝜓 ⊻ 𝜒 ) ) )