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

Theorem comcom4 455
Description: Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
Hypothesis
Ref Expression
comcom.1 a C b
Assertion
Ref Expression
comcom4 a C b

Proof of Theorem comcom4
StepHypRef Expression
1 comcom.1 . . 3 a C b
21comcom3 454 . 2 a C b
32comcom2 183 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:  comd  456  comcom5  458  fh3  471  fh4  472  com2an  484  gstho  491  i3abs3  524  u2lemc4  702  u3lemc4  703  u4lemc4  704  u5lemc4  705  u2lem3  750  u4lem4  759  u5lem5  765  u5lem6  769  3vded3  819  marsdenlem1  880  marsdenlem2  881
  Copyright terms: Public domain W3C validator