Theorem xorass 1308

Description: ⊻ is associative. (Contributed by FL, 22-Nov-2010.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)

Assertion

Ref	Expression
xorass	⊢ (((φ ⊻ ψ) ⊻ χ) ↔ (φ ⊻ (ψ ⊻ χ)))

Proof of Theorem xorass

Step	Hyp	Ref	Expression
1		biass 348	. . . . . 6 ⊢ (((φ ↔ ψ) ↔ χ) ↔ (φ ↔ (ψ ↔ χ)))
2	1	notbii 287	. . . . 5 ⊢ (¬ ((φ ↔ ψ) ↔ χ) ↔ ¬ (φ ↔ (ψ ↔ χ)))
3		nbbn 347	. . . . 5 ⊢ ((¬ (φ ↔ ψ) ↔ χ) ↔ ¬ ((φ ↔ ψ) ↔ χ))
4		pm5.18 345	. . . . . 6 ⊢ ((φ ↔ (ψ ↔ χ)) ↔ ¬ (φ ↔ ¬ (ψ ↔ χ)))
5	4	con2bii 322	. . . . 5 ⊢ ((φ ↔ ¬ (ψ ↔ χ)) ↔ ¬ (φ ↔ (ψ ↔ χ)))
6	2, 3, 5	3bitr4i 268	. . . 4 ⊢ ((¬ (φ ↔ ψ) ↔ χ) ↔ (φ ↔ ¬ (ψ ↔ χ)))
7		df-xor 1305	. . . . 5 ⊢ ((φ ⊻ ψ) ↔ ¬ (φ ↔ ψ))
8	7	bibi1i 305	. . . 4 ⊢ (((φ ⊻ ψ) ↔ χ) ↔ (¬ (φ ↔ ψ) ↔ χ))
9		df-xor 1305	. . . . 5 ⊢ ((ψ ⊻ χ) ↔ ¬ (ψ ↔ χ))
10	9	bibi2i 304	. . . 4 ⊢ ((φ ↔ (ψ ⊻ χ)) ↔ (φ ↔ ¬ (ψ ↔ χ)))
11	6, 8, 10	3bitr4i 268	. . 3 ⊢ (((φ ⊻ ψ) ↔ χ) ↔ (φ ↔ (ψ ⊻ χ)))
12	11	notbii 287	. 2 ⊢ (¬ ((φ ⊻ ψ) ↔ χ) ↔ ¬ (φ ↔ (ψ ⊻ χ)))
13		df-xor 1305	. 2 ⊢ (((φ ⊻ ψ) ⊻ χ) ↔ ¬ ((φ ⊻ ψ) ↔ χ))
14		df-xor 1305	. 2 ⊢ ((φ ⊻ (ψ ⊻ χ)) ↔ ¬ (φ ↔ (ψ ⊻ χ)))
15	12, 13, 14	3bitr4i 268	1 ⊢ (((φ ⊻ ψ) ⊻ χ) ↔ (φ ⊻ (ψ ⊻ χ)))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 176   ⊻ wxo 1304

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-xor 1305

This theorem is used by:  hadass  1386