Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xorass Structured version   Unicode version

Theorem xorass 1364
 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
StepHypRef Expression
1 biass 359 . . . . . 6
21notbii 296 . . . . 5
3 nbbn 358 . . . . 5
4 pm5.18 356 . . . . . 6
54con2bii 332 . . . . 5
62, 3, 53bitr4i 277 . . . 4
7 df-xor 1361 . . . . 5
87bibi1i 314 . . . 4
9 df-xor 1361 . . . . 5
109bibi2i 313 . . . 4
116, 8, 103bitr4i 277 . . 3
1211notbii 296 . 2
13 df-xor 1361 . 2
14 df-xor 1361 . 2
1512, 13, 143bitr4i 277 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 184   wxo 1360 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 185  df-xor 1361 This theorem is referenced by:  hadass  1437
 Copyright terms: Public domain W3C validator