Theorem xorass 1506

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 386	. . 3 ⊢ (¬ (𝜑 ↔ (𝜓 ⊻ 𝜒)) ↔ (𝜑 ↔ ¬ (𝜓 ⊻ 𝜒)))
2		biass 388	. . . 4 ⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒)))
3		xnor 1503	. . . . 5 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ⊻ 𝜓))
4	3	bibi1i 341	. . . 4 ⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (¬ (𝜑 ⊻ 𝜓) ↔ 𝜒))
5		xnor 1503	. . . . 5 ⊢ ((𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ⊻ 𝜒))
6	5	bibi2i 340	. . . 4 ⊢ ((𝜑 ↔ (𝜓 ↔ 𝜒)) ↔ (𝜑 ↔ ¬ (𝜓 ⊻ 𝜒)))
7	2, 4, 6	3bitr3i 303	. . 3 ⊢ ((¬ (𝜑 ⊻ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ ¬ (𝜓 ⊻ 𝜒)))
8		nbbn 387	. . 3 ⊢ ((¬ (𝜑 ⊻ 𝜓) ↔ 𝜒) ↔ ¬ ((𝜑 ⊻ 𝜓) ↔ 𝜒))
9	1, 7, 8	3bitr2ri 302	. 2 ⊢ (¬ ((𝜑 ⊻ 𝜓) ↔ 𝜒) ↔ ¬ (𝜑 ↔ (𝜓 ⊻ 𝜒)))
10		df-xor 1502	. 2 ⊢ (((𝜑 ⊻ 𝜓) ⊻ 𝜒) ↔ ¬ ((𝜑 ⊻ 𝜓) ↔ 𝜒))
11		df-xor 1502	. 2 ⊢ ((𝜑 ⊻ (𝜓 ⊻ 𝜒)) ↔ ¬ (𝜑 ↔ (𝜓 ⊻ 𝜒)))
12	9, 10, 11	3bitr4i 305	1 ⊢ (((𝜑 ⊻ 𝜓) ⊻ 𝜒) ↔ (𝜑 ⊻ (𝜓 ⊻ 𝜒)))

Syntax hints:  ¬ wn 3   ↔ wb 208   ⊻ wxo 1501

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 209  df-xor 1502

This theorem is referenced by:  hadass  1597  symdifass  4230