QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  letr Unicode version
Theorem letr 137
Description: Transitive law for l.e.
Hypotheses
Ref Expression
letr.1 a =< b
letr.2 b =< c
Assertion
Ref Expression
letr a =< c
Proof of Theorem letr
StepHypRef Expression
1 letr.1 . . . . . . . 8 a =< b
21df-le2 131 . . . . . . 7 (a v b) = b
32ax-r5 38 . . . . . 6 ((a v b) v c) = (b v c)
43ax-r1 35 . . . . 5 (b v c) = ((a v b) v c)
5 letr.2 . . . . . 6 b =< c
65df-le2 131 . . . . 5 (b v c) = c
7 ax-a3 32 . . . . 5 ((a v b) v c) = (a v (b v c))
84, 6, 73tr2 64 . . . 4 c = (a v (b v c))
98lan 77 . . 3 (a ^ c) = (a ^ (a v (b v c)))
10 anabs 121 . . 3 (a ^ (a v (b v c))) = a
119, 10ax-r2 36 . 2 (a ^ c) = a
1211df2le1 135 1 a =< c
Colors of variables: term
Syntax hints:   =< wle 2   v 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:  leao1  162  leao2  163  leao3  164  leao4  165  le2or  168  le2an  169  distlem  188  str  189  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  ka4lemo  228  ska13  241  womle  298  nom20  313  nom21  314  nom22  315  wom3  367  ska2  432  gsth  489  i3bi  496  df2i3  498  dfi3b  499  oi3ai3  503  binr2  518  i3con  551  i3orlem2  553  i3orlem3  554  i3orlem7  558  ud3lem1a  566  ud3lem1c  568  ud3lem1d  569  ud3lem3a  572  ud3lem3d  575  ud3lem3  576  ud4lem1b  578  ud4lem1c  579  ud4lem1  581  ud5lem1b  587  ud5lem1  589  u4lemona  628  u1lemob  630  u3lemob  632  u5lemob  634  u1lemc6  706  comi12  707  u12lembi  726  u4lem1  737  u4lem2  747  u4lem6  768  u1lem8  776  u1lem9ab  779  u3lem13b  790  u3lem14mp  794  bi1o1a  798  test2  803  3vth1  804  3vded12  815  3vded22  818  1oa  820  2oalem1  825  oale  829  oaeqv  830  mlalem  832  eqtr4  834  sa5  836  sadm3  838  bi3  839  imp3  841  orbi  842  mlaconj4  844  mlaconj2  846  negantlem2  849  negantlem3  850  negantlem9  859  negantlem10  861  neg3antlem1  864  neg3antlem2  865  elimconslem  867  elimcons  868  comanblem1  870  comanb  872  mhlemlem1  874  mhlem  876  mh  879  mlaconjo  886  oago3.21x  890  cancellem  891  kb10iii  893  gon2n  898  gomaex3lem10  923  oas  925  oasr  926  oat  927  oatr  928  oaur  930  oaidlem2  931  oaidlem2g  932  oal42  935  oa4lem3  939  oa3to4lem1  945  oa3to4lem2  946  oa3to4lem4  948  oa4b  959  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa4to6dual  964  oa4btoc  966  oa4to4u2  974  oa4uto4g  975  oa4uto4  977  oa3-u1lem  985  oa3-u1  991  oa3-1to5  993  d3oa  995  d4oa  996  oaliv  1003  oadist2a  1007  oacom2  1012  oagen2  1016  oagen2b  1017  mloa  1018  oadist  1019  oadistc0  1021  oadistc  1022  oadistd  1023  axoa4  1034  4oadist  1044  lem3.3.5  1055  dp15lema  1152  dp15lemh  1159  dp53lema  1161  dp53lemd  1164  dp53leme  1165  dp53lemf  1166  dp53lemg  1167  dp35leme  1171  dp35lemd  1172  dp35lema  1176  dp35lem0  1177  dp34  1179  dp41lemh  1188  dp41lemm  1192  dp23  1195  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206
  Copyright terms: Public domain W3C validator