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

Theorem comor2 462
Description: Commutation law. (Contributed by NM, 9-Nov-1997.)
Assertion
Ref Expression
comor2 (ab) C b

Proof of Theorem comor2
StepHypRef Expression
1 ax-a2 31 . 2 (ab) = (ba)
2 comor1 461 . 2 (ba) C b
31, 2bctr 181 1 (ab) C b
Colors of variables: term
Syntax hints:   C wc 3  wo 6
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:  comorr2  463  oml6  488  gsth2  490  dfi3b  499  i3con  551  i3orlem7  558  i3orlem8  559  ud1lem3  562  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem1d  569  ud3lem3d  575  ud3lem3  576  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud4lem3b  584  ud4lem3  585  ud5lem1  589  ud5lem3  594  u4lemana  608  u4lemoa  623  u4lemona  628  u3lemob  632  u3lemonb  637  u4lemle2  718  u4lem1  737  u4lem5  764  u4lem6  768  u1lem11  780  u3lem11  786  u3lem15  795  test  802  test2  803  3vded21  817  neg3antlem2  865  mhlem  876  mhlem1  877
  Copyright terms: Public domain W3C validator