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

Theorem leao2 163
Description: L.e. absorption. (Contributed by NM, 8-Jul-2000.)
Assertion
Ref Expression
leao2 (ba) ≤ (ac)

Proof of Theorem leao2
StepHypRef Expression
1 lear 161 . 2 (ba) ≤ a
2 leo 158 . 2 a ≤ (ac)
31, 2letr 137 1 (ba) ≤ (ac)
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:  bi4  840  negantlem10  861  mhlem1  877  mhlem2  878  mh  879  mhcor1  888  lem4.6.7  1103  vneulem6  1136  vneulem7  1137  vneulemexp  1148  dp32  1196
  Copyright terms: Public domain W3C validator