QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  anass Unicode version
Theorem anass 76
Description: Associative law.
Assertion
Ref Expression
anass ((a ^ b) ^ c) = (a ^ (b ^ c))
Proof of Theorem anass
StepHypRef Expression
1 ax-a3 32 . . . 4 ((a' v b') v c') = (a' v (b' v c'))
2 df-a 40 . . . . . 6 (a ^ b) = (a' v b')'
32con2 67 . . . . 5 (a ^ b)' = (a' v b')
43ax-r5 38 . . . 4 ((a ^ b)' v c') = ((a' v b') v c')
5 df-a 40 . . . . . 6 (b ^ c) = (b' v c')'
65con2 67 . . . . 5 (b ^ c)' = (b' v c')
76lor 70 . . . 4 (a' v (b ^ c)') = (a' v (b' v c'))
81, 4, 73tr1 63 . . 3 ((a ^ b)' v c') = (a' v (b ^ c)')
98ax-r4 37 . 2 ((a ^ b)' v c')' = (a' v (b ^ c)')'
10 df-a 40 . 2 ((a ^ b) ^ c) = ((a ^ b)' v c')'
11 df-a 40 . 2 (a ^ (b ^ c)) = (a' v (b ^ c)')'
129, 10, 113tr1 63 1 ((a ^ b) ^ c) = (a ^ (b ^ c))
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40
This theorem is referenced by:  an12  81  an32  83  an4  86  mi  125  wanass  204  wwcom3ii  215  wwfh1  216  wwfh2  217  ska6  234  nom11  308  nom14  311  nom15  312  nom21  314  nom24  317  nom25  318  k1-6  353  k1-7  354  2vwomlem  365  wr5-2v  366  wcomlem  382  wcom3ii  419  wfh1  423  wfh2  424  oml5a  450  comcom  453  com3ii  457  fh1  469  fh2  470  oml4  487  gsth  489  i3bi  496  dfi3b  499  i3lem1  504  lem4  511  i3orlem8  559  ud3lem1a  566  ud3lem1b  567  ud3lem2  571  ud3lem3b  573  ud4lem1a  577  ud4lem1b  578  ud4lem2  582  ud4lem3a  583  ud5lem1a  586  ud5lem1b  587  ud5lem1c  588  ud5lem3a  591  ud5lem3b  592  ud5lem3c  593  u2lemaa  601  u3lemaa  602  u4lemaa  603  u5lemaa  604  u1lemab  610  u3lemab  612  u4lemab  613  u5lemab  614  u1lemanb  615  u2lemanb  616  u3lemanb  617  u4lemanb  618  u5lemanb  619  u1lemle2  715  u2lemle2  716  u4lemle2  718  u5lemle2  719  u21lembi  727  u1lem4  757  u4lem5  764  u4lem6  768  u24lem  770  u2lem8  782  u3lem10  785  u3lem11  786  u3lem15  795  3vth1  804  3vth7  810  3vth9  812  3vded21  817  1oa  820  1oaiii  823  2oath1  826  oale  829  mlalem  832  mlaoml  833  bi3  839  bi4  840  mlaconj4  844  mlaconj  845  elimcons2  869  comanblem1  870  comanblem2  871  mh  879  mhcor1  888  oago3.29  889  cancellem  891  govar  896  go2n4  899  go2n6  901  oaidlem2  931  oaidlem2g  932  oa3to4lem1  945  oa3to4lem2  946  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  d4oa  996  oaliii  1001  oalem1  1005  oagen1b  1015  oadist  1019  oadistb  1020  oa3moa3  1029  4oagen1b  1043  lem3.3.4  1053  lem3.3.6  1056  lem3.3.7i1e2  1061  lem3.3.7i3e1  1066  lem4.6.2e1  1080  vneulem2  1130  vneulemexp  1146  modexp  1150  dp53lemb  1162  dp53lemf  1166  dp35leme  1171  dp35lemb  1174  dp41lemb  1181  dp41lemc  1183  dp41leme  1185  xdp41  1196  xdp53  1198  xxdp41  1199  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  testmod2  1213  testmod2expanded  1214
  Copyright terms: Public domain W3C validator