QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  comanr1 GIF version

Theorem comanr1 464
Description: Commutation law. (Contributed by NM, 26-Nov-1997.)
Assertion
Ref Expression
comanr1 a C (ab)

Proof of Theorem comanr1
StepHypRef Expression
1 coman1 185 . 2 (ab) C a
21comcom 453 1 a C (ab)
Colors of variables: term
Syntax hints:   C wc 3  wa 7
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  combi  485  ud3lem1a  566  ud5lem3a  591  ud5lem3b  592  ud5lem3  594  u1lemaa  600  u3lemaa  602  u4lemaa  603  u5lemaa  604  u3lemana  607  u4lemana  608  u5lemana  609  u1lemc1  680  u5lemc1  684  u4lemle2  718  u5lemle2  719  u21lembi  727  u4lem1  737  u4lem4  759  u24lem  770  u1lem11  780  u3lem10  785  u3lem13a  789  u3lem13b  790  bi1o1a  798  i1abs  801  3vth9  812  mlalem  832  bi3  839  bi4  840  imp3  841  mlaconj4  844  comanblem1  870  comanblem2  871  oas  925
  Copyright terms: Public domain W3C validator