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

Theorem leran 153
Description: Add conjunct to right of both sides. (Contributed by NM, 27-Aug-1997.)
Hypothesis
Ref Expression
le.1 ab
Assertion
Ref Expression
leran (ac) ≤ (bc)

Proof of Theorem leran
StepHypRef Expression
1 anandir 115 . . . 4 ((ab) ∩ c) = ((ac) ∩ (bc))
21ax-r1 35 . . 3 ((ac) ∩ (bc)) = ((ab) ∩ c)
3 le.1 . . . . 5 ab
43df2le2 136 . . . 4 (ab) = a
54ran 78 . . 3 ((ab) ∩ c) = (ac)
62, 5ax-r2 36 . 2 ((ac) ∩ (bc)) = (ac)
76df2le1 135 1 (ac) ≤ (bc)
Colors of variables: term
Syntax hints:  wle 2  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-t 41  df-f 42  df-le1 130  df-le2 131
This theorem is referenced by:  lelan  167  le2an  169  i2or  344  i5lei4  350  k1-8a  355  3vth1  804  3vded21  817  3vded22  818  1oaiii  823  3vroa  831  eqtr4  834  sadm3  838  negantlem3  850  comanblem1  870  mh  879  gomaex4  900  oasr  926  oa3-u2lem  986  d4oa  996  oaliii  1001  oagen2b  1017  axoa4  1034  lem3.4.3  1076  lem4.6.7  1103  ml  1123  dp15lema  1154  dp15leme  1158  dp41lemh  1190  dp41leml  1193  xdp41  1198  xdp15  1199  xxdp41  1201  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208
  Copyright terms: Public domain W3C validator