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

Theorem lerr 150
 Description: Add disjunct to right of l.e.
Hypothesis
Ref Expression
le.1 ab
Assertion
Ref Expression
lerr a ≤ (cb)

Proof of Theorem lerr
StepHypRef Expression
1 le.1 . . 3 ab
21ler 149 . 2 a ≤ (bc)
3 ax-a2 31 . 2 (bc) = (cb)
42, 3lbtr 139 1 a ≤ (cb)
 Colors of variables: term Syntax hints:   ≤ wle 2   ∪ 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 This theorem depends on definitions:  df-a 40  df-le1 130  df-le2 131 This theorem is referenced by:  i3orlem6  557  1oa  820  mhlem  876  marsdenlem3  882  cancellem  891  lem3.3.7i4e1  1069  lem4.6.6i2j1  1094  lem4.6.6i2j4  1095  lem4.6.6i3j1  1097  lem4.6.6i4j2  1099  vneulem6  1134  vneulemexp  1146  l42modlem1  1147  dp53lemc  1163  dp35lemc  1173  dp32  1194  xdp53  1198  xxdp53  1201  xdp43lem  1203  xdp43  1205  3dp43  1206  oadp35lemc  1209
 Copyright terms: Public domain W3C validator