Theorem bltr 130

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 37	. . 3 (a v c) = (b v c)
3		bltr.2	. . . 4 b =< c
4	3	df-le2 123	. . 3 (b v c) = c
5	2, 4	ax-r2 35	. 2 (a v c) = c
6	5	df-le1 122	1 a =< c

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

This theorem is referenced by:  le3tr1 132  lear 153  ler2or 164  ler2an 165  ledi 166  ledio 168  ka4lemo 220  ska13 233  wlem1 235  ska15 236  wql1lem 279  wql2lem 280  womle2a 287  womle 290  i2or 336  i1or 337  i5lei1 339  2vwomlem 347  wr5-2v 348  ska2 414  ska4 415  oml4 469  gsth 471  cmtr1com 475  i3bi 478  i3or 479  bii3 498  i3th5 529  i3con 533  i3orlem3 536  i3orlem8 541  ud3lem3a 554  ud4lem1b 560  comi1 691  i2bi 704  u1lem9a 759  u3lemax4 778  u3lemax5 779  test2 785  3vth1 786  3vth2 787  3vded11 796  3vded12 797  3vded13 798  3vded22 800  1oa 802  1oaiii 805  1oaii 806  2oalem1 807  3vroa 813  mlalem 814  mlaoml 815  sa5 818  sadm3 820  bi3 821  bi4 822  orbile 825  mlaconj4 826  negantlem2 831  negantlem4 833  negantlem9 841  negantlem10 843  elimconslem 849  elimcons 850  comanblem1 852  mh 861  distid 869  oago3.29 871  oago3.21x 872  cancellem 873  kb10iii 875  govar 876  go2n4 879  gomaex4 880  go2n6 881  gomaex3h4 885  gomaex3h5 886  gomaex3lem7 900  gomaex3lem8 901  gomaex3lem9 902  gomaex3 904  oas 905  oat 907  oaidlem2 911  oaidlem2g 912  oa23 916  distoa 924  oa4to4u2 954  oa4uto4g 955  oa4gto4u 956  oa4uto4 957  oa3-u2lem 966  oa3-6to3 967  oa3-2to4 968  oa3-2to2s 970  oa3-u1 971  oa3-u2 972  d3oa 975  d4oa 976  oaliii 981  oalii 982  oalem1 985  oadist2a 987  mloa 998  oadist 999  oadistb 1000  oadistc0 1001  oadistd 1003  3oa3 1005  oa43v 1008  oa63v 1011  axoa4d 1017  4oa 1018  4oadist 1023

This theorem was proved from axioms:  ax-r2 35  ax-r5 37

This theorem depends on definitions:  df-le1 122  df-le2 123

metamath.org