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

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

Syntax hints:   = wb 1   =< wle 2   v wo 6

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  dplem15a 1148  dplem15e 1152  dp53lema 1157  dp53leme 1161  dp53lemf 1162  dp41lema 1166  dp41lemb 1167  dp41lemc 1169  dp41leme 1171  dp41lemh 1174  dp41leml 1177  dp41lemm 1178

This theorem was proved from axioms:  ax-r2 36  ax-r5 38

This theorem depends on definitions:  df-le1 130  df-le2 131

Copyright terms: Public domain