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

Theorem lelan 167
Description: Add conjunct to left of both sides.
Hypothesis
Ref Expression
lel.1 ab
Assertion
Ref Expression
lelan (ca) ≤ (cb)

Proof of Theorem lelan
StepHypRef Expression
1 lel.1 . . 3 ab
21leran 153 . 2 (ac) ≤ (bc)
3 ancom 74 . 2 (ca) = (ac)
4 ancom 74 . 2 (cb) = (bc)
52, 3, 4le3tr1 140 1 (ca) ≤ (cb)
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:  le2an  169  go1  343  i1or  345  i5lei3  349  wr5-2v  366  ortha  438  gsth  489  ud4lem1a  577  test  802  3vded11  814  mlaconj  845  elimconslem  867  elimcons  868  kb10iii  893  oas  925  oatr  928  oaur  930  oaidlem2  931  oaidlem2g  932  oa3to4lem1  945  oa3to4lem2  946  oa3to4lem3  947  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa4to6lem4  963  oa4btoc  966  oa4uto4g  975  oa4uto4  977  oa3-1to5  993  oalem1  1005  oadist2a  1007  oagen1  1014  oagen2  1016  oadistc0  1021  oadistd  1023  4oagen1  1042  4oadist  1044  lem3.3.5  1055  dp15lemf  1157  dp35lem0  1177  dp41lemc  1183  dp41lemh  1188  dp41leml  1191  xdp41  1196  xdp15  1197  xxdp41  1199  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206
  Copyright terms: Public domain W3C validator