QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  lbtr Unicode version
Theorem lbtr 139
Description: Transitive inference.
Hypotheses
Ref Expression
lbtr.1 a =< b
lbtr.2 b = c
Assertion
Ref Expression
lbtr a =< c
Proof of Theorem lbtr
StepHypRef Expression
1 lbtr.2 . . . . 5 b = c
21ax-r1 35 . . . 4 c = b
32lan 77 . . 3 (a ^ c) = (a ^ b)
4 lbtr.1 . . . 4 a =< b
54df2le2 136 . . 3 (a ^ b) = a
63, 5ax-r2 36 . 2 (a ^ c) = a
76df2le1 135 1 a =< c
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2   ^ wa 7
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  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:  le3tr1  140  lerr  150  lecon2  156  leor  159  lel2or  170  lel2an  171  ledi  174  ledio  176  ka4lemo  228  wlem1  243  ska15  244  bina4  285  bina5  286  womle2b  296  womle3b  297  nom14  311  nom20  313  nom23  316  nom24  317  go1  343  i2or  344  i1or  345  k1-8a  355  k1-8b  356  wom2  434  ka4ot  435  ortha  438  i3bi  496  lem4  511  binr3  519  i3th5  547  i3th7  549  i3th8  550  i3orlem1  552  i3orlem4  555  i3orlem7  558  i3orlem8  559  ud3lem1c  568  ud4lem1c  579  u1lemc6  706  i2bi  722  u12lembi  726  u1lem9b  778  u3lem14mp  794  3vth6  809  3vded11  814  3vded12  815  3vded21  817  3vded22  818  oaeqv  830  sadm3  838  bi3  839  bi4  840  mlaconj4  844  mlaconj  845  negantlem1  848  negantlem2  849  negantlem3  850  negantlem9  859  negantlem10  861  neg3antlem1  864  neg3antlem2  865  neg3ant1  866  elimconslem  867  elimcons  868  mhlem  876  mhlem2  878  marsdenlem3  882  marsdenlem4  883  mlaconjolem  885  mlaconjo  886  mhcor1  888  oago3.29  889  oago3.21x  890  cancellem  891  kb10iii  893  e2ast2  894  govar2  897  gomaex4  900  gomaex3h3  904  gomaex3h6  907  gomaex3h7  908  gomaex3h8  909  gomaex3lem4  917  oas  925  oat  927  oatr  928  oau  929  oaur  930  oal42  935  oa23  936  oa4lem1  937  oa4lem2  938  oa3to4lem1  945  oa3to4lem2  946  oa6to4h1  955  oa6to4h2  956  oa6to4h3  957  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa4btoc  966  oa3-u2lem  986  oa3-2to2s  990  oa3-1to5  993  d3oa  995  d4oa  996  oaliv  1003  oalem1  1005  oadist2a  1007  oadist2b  1008  oagen1  1014  oagen2  1016  mloa  1018  oadistc0  1021  oadistc  1022  oadistd  1023  oa4cl  1027  oa3moa3  1029  axoa4a  1037  4oagen1  1042  4oadist  1044  lem3.3.5  1055  lem3.4.3  1076  lem4.6.7  1101  ml3le  1127  vneulem7  1135  vneulemexp  1146  l42mod  1149  dp15lema  1152  dp15leme  1156  dp15lemf  1157  dp15lemh  1159  dp53lema  1161  dp53lemc  1163  dp53lemd  1164  dp53lemf  1166  dp35lemd  1172  dp35lemc  1173  dp35lembb  1175  dp35lem0  1177  dp34  1179  dp41leml  1191  dp41lemm  1192  dp32  1194  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  oadp35lemc  1209
  Copyright terms: Public domain W3C validator