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 1031  axoa4d 1037  4oa 1038  4oadist 1043  lem3.3.3lem1 1048  lem3.3.5 1054  lem3.4.3 1075  wdwom 1103

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