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

Theorem comcom6 459
Description: Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 26-Nov-1997.)
Hypothesis
Ref Expression
comcom6.1 a C b
Assertion
Ref Expression
comcom6 a C b

Proof of Theorem comcom6
StepHypRef Expression
1 comcom6.1 . . 3 a C b
21comcom2 183 . 2 a C b
32comcom5 458 1 a C b
Colors of variables: term
Syntax hints:   C wc 3   wn 4
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  ud3lem1c  568  ud5lem3a  591  ud5lem3b  592  ud5lem3  594  u3lemaa  602  u4lemaa  603  u5lemaa  604  u3lemab  612  u4lemab  613  u5lemab  614  u2lemc1  681  u5lemc1  684  u5lemc1b  685  u1lemc6  706  u4lemle2  718  u5lemle2  719  u4lem5  764  u24lem  770  u3lem7  774  i1abs  801  3vth7  810  3vth9  812  3vcom  813  2oalem1  825  oale  829  bi4  840  negantlem1  848  elimconslem  867  comanblem2  871  mhlem1  877  marsdenlem2  881  oas  925  lem4.6.2e1  1082  lem4.6.6i1j3  1094
  Copyright terms: Public domain W3C validator