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