QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  bltr Unicode version
Theorem bltr 138
Description: Transitive inference.
Hypotheses
Ref Expression
bltr.1 a = b
bltr.2 b =< c
Assertion
Ref Expression
bltr a =< c
Proof of Theorem bltr
StepHypRef Expression
1 bltr.1 . . . 4 a = b
21ax-r5 38 . . 3 (a v c) = (b v c)
3 bltr.2 . . . 4 b =< c
43df-le2 131 . . 3 (b v c) = c
52, 4ax-r2 36 . 2 (a v c) = c
65df-le1 130 1 a =< c
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2   v wo 6
This theorem was proved from axioms:  ax-r2 36  ax-r5 38
This theorem depends on definitions:  df-le1 130  df-le2 131
This theorem is referenced by:  le3tr1  140  lear  161  ler2or  172  ler2an  173  ledi  174  ledio  176  ka4lemo  228  ska13  241  wlem1  243  ska15  244  wql1lem  287  wql2lem  288  womle2a  295  womle  298  i2or  344  i1or  345  i5lei1  347  id5leid0  351  2vwomlem  365  wr5-2v  366  ska2  432  ska4  433  oml4  487  gsth  489  cmtr1com  493  i3bi  496  i3or  497  bii3  516  i3th5  547  i3con  551  i3orlem3  554  i3orlem8  559  ud3lem3a  572  ud4lem1b  578  comi1  709  i2bi  722  u1lem9a  777  u3lemax4  796  u3lemax5  797  test2  803  3vth1  804  3vth2  805  3vded11  814  3vded12  815  3vded13  816  3vded22  818  1oa  820  1oaiii  823  1oaii  824  2oalem1  825  3vroa  831  mlalem  832  mlaoml  833  sa5  836  sadm3  838  bi3  839  bi4  840  orbile  843  mlaconj4  844  negantlem2  849  negantlem4  851  negantlem9  859  negantlem10  861  elimconslem  867  elimcons  868  comanblem1  870  mh  879  distid  887  oago3.29  889  oago3.21x  890  cancellem  891  kb10iii  893  govar  896  go2n4  899  gomaex4  900  go2n6  901  gomaex3h4  905  gomaex3h5  906  gomaex3lem7  920  gomaex3lem8  921  gomaex3lem9  922  gomaex3  924  oas  925  oat  927  oaidlem2  931  oaidlem2g  932  oa23  936  distoa  944  oa4to4u2  974  oa4uto4g  975  oa4gto4u  976  oa4uto4  977  oa3-u2lem  986  oa3-6to3  987  oa3-2to4  988  oa3-2to2s  990  oa3-u1  991  oa3-u2  992  d3oa  995  d4oa  996  oaliii  1001  oalii  1002  oalem1  1005  oadist2a  1007  mloa  1018  oadist  1019  oadistb  1020  oadistc0  1021  oadistd  1023  3oa3  1025  oa43v  1028  oa63v  1032  axoa4d  1038  4oa  1039  4oadist  1044  lem3.3.3lem1  1049  lem3.3.5  1055  lem3.4.3  1076  wdwom  1104  vneulem6  1134  vneulemexp  1146  dp15lema  1152  dp15leme  1156  dp53lema  1161  dp53leme  1165  dp53lemf  1166  dp35leme  1171  dp35lemd  1172  dp35lem0  1177  dp41lema  1180  dp41lemb  1181  dp41lemc  1183  dp41leme  1185  dp41lemh  1188  dp41leml  1191  dp41lemm  1192  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