This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( ( 𝜑 ⊻ 𝜓 ) ⊻ 𝜒 ) ↔ ( 𝜑 ⊻ ( 𝜓 ⊻ 𝜒 ) ) )