Theorem xorass 1508

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.)

Assertion

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

Proof of Theorem xorass

Step	Hyp	Ref	Expression
1		xor3 383	. . 3 ⊢ (¬ (𝜑 ↔ (𝜓 ⊻ 𝜒)) ↔ (𝜑 ↔ ¬ (𝜓 ⊻ 𝜒)))
2		biass 385	. . . 4 ⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))
3		xnor 1505	. . . . 5 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ⊻ 𝜓))
4	3	bibi1i 338	. . . 4 ⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (¬ (𝜑 ⊻ 𝜓) ↔ 𝜒))
5		xnor 1505	. . . . 5 ⊢ ((𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ⊻ 𝜒))
6	5	bibi2i 337	. . . 4 ⊢ ((𝜑 ↔ (𝜓 ↔ 𝜒)) ↔ (𝜑 ↔ ¬ (𝜓 ⊻ 𝜒)))
7	2, 4, 6	3bitr3i 300	. . 3 ⊢ ((¬ (𝜑 ⊻ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ ¬ (𝜓 ⊻ 𝜒)))
8		nbbn 384	. . 3 ⊢ ((¬ (𝜑 ⊻ 𝜓) ↔ 𝜒) ↔ ¬ ((𝜑 ⊻ 𝜓) ↔ 𝜒))
9	1, 7, 8	3bitr2ri 299	. 2 ⊢ (¬ ((𝜑 ⊻ 𝜓) ↔ 𝜒) ↔ ¬ (𝜑 ↔ (𝜓 ⊻ 𝜒)))
10		df-xor 1504	. 2 ⊢ (((𝜑 ⊻ 𝜓) ⊻ 𝜒) ↔ ¬ ((𝜑 ⊻ 𝜓) ↔ 𝜒))
11		df-xor 1504	. 2 ⊢ ((𝜑 ⊻ (𝜓 ⊻ 𝜒)) ↔ ¬ (𝜑 ↔ (𝜓 ⊻ 𝜒)))
12	9, 10, 11	3bitr4i 302	1 ⊢ (((𝜑 ⊻ 𝜓) ⊻ 𝜒) ↔ (𝜑 ⊻ (𝜓 ⊻ 𝜒)))

Syntax hints:  ¬ wn 3   ↔ wb 205   ⊻ wxo 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-xor 1504

This theorem is referenced by:  hadass  1599  symdifass  4182  wl-df3xor3  35568