Theorem bltr 138

Description: Transitive inference. (Contributed by NM, 28-Aug-1997.)

Hypotheses

Ref	Expression
bltr.1	a = b
bltr.2	b ≤ c

Assertion

Ref	Expression
bltr	a ≤ c

Proof of Theorem bltr

Step	Hyp	Ref	Expression
1		bltr.1	. . . 4 a = b
2	1	ax-r5 38	. . 3 (a ∪ c) = (b ∪ c)
3		bltr.2	. . . 4 b ≤ c
4	3	df-le2 131	. . 3 (b ∪ c) = c
5	2, 4	ax-r2 36	. 2 (a ∪ c) = c
6	5	df-le1 130	1 a ≤ c

Syntax hints:   = wb 1   ≤ wle 2   ∪ 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  1106  vneulem6  1136  vneulemexp  1148  dp15lema  1154  dp15leme  1158  dp53lema  1163  dp53leme  1167  dp53lemf  1168  dp35leme  1173  dp35lemd  1174  dp35lem0  1179  dp41lema  1182  dp41lemb  1183  dp41lemc  1185  dp41leme  1187  dp41lemh  1190  dp41leml  1193  dp41lemm  1194  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208