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

Theorem leao4 165
Description: L.e. absorption. (Contributed by NM, 8-Jul-2000.)
Assertion
Ref Expression
leao4 (ba) ≤ (ca)

Proof of Theorem leao4
StepHypRef Expression
1 lear 161 . 2 (ba) ≤ a
2 leor 159 . 2 a ≤ (ca)
31, 2letr 137 1 (ba) ≤ (ca)
Colors of variables: term
Syntax hints:  wle 2  wo 6  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
This theorem depends on definitions:  df-a 40  df-le1 130  df-le2 131
This theorem is referenced by:  k1-4  359  u3lem15  795  bi4  840  negantlem9  859  negantlem10  861  mh  879  marsdenlem4  883  cancellem  891  e2ast2  894  lem4.6.6i0j4  1091  lem4.6.6i2j4  1097  lem4.6.6i3j1  1099  lem4.6.6i4j0  1100  lem4.6.6i4j2  1101  dp53lemf  1168  xdp53  1200  xxdp53  1203  xdp43lem  1205  xdp43  1207  3dp43  1208
  Copyright terms: Public domain W3C validator