Metamath Proof Explorer

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 ⊢ φ ⊻ ψ ⊻ χ ↔ φ ⊻ ψ ⊻ χ