Theorem lbtr 131

Description: Transitive inference.

Hypotheses

Ref	Expression
lbtr.1	a =< b
lbtr.2	b = c

Assertion

Ref	Expression
lbtr	a =< c

Proof of Theorem lbtr

Step	Hyp	Ref	Expression
1		lbtr.2	. . . . 5 b = c
2	1	ax-r1 34	. . . 4 c = b
3	2	lan 70	. . 3 (a ^ c) = (a ^ b)
4		lbtr.1	. . . 4 a =< b
5	4	df2le2 128	. . 3 (a ^ b) = a
6	3, 5	ax-r2 35	. 2 (a ^ c) = a
7	6	df2le1 127	1 a =< c

Syntax hints:   = wb 1   =< wle 2   ^ wa 7

This theorem is referenced by:  le3tr1 132  lerr 142  lecon2 148  leor 151  lel2or 162  lel2an 163  ledi 166  ledio 168  ka4lemo 220  wlem1 235  ska15 236  bina4 277  bina5 278  womle2b 288  womle3b 289  nom14 303  nom20 305  nom23 308  nom24 309  go1 335  i2or 336  i1or 337  wr5 413  wom2 416  ka4ot 417  ortha 420  i3bi 478  lem4 493  binr3 501  i3th5 529  i3th7 531  i3th8 532  i3orlem1 534  i3orlem4 537  i3orlem7 540  i3orlem8 541  ud3lem1c 550  ud4lem1c 561  u1lemc6 688  i2bi 704  u12lembi 708  u1lem9b 760  u3lem14mp 776  3vth6 791  3vded11 796  3vded12 797  3vded21 799  3vded22 800  oaeqv 812  sadm3 820  bi3 821  bi4 822  mlaconj4 826  mlaconj 827  negantlem1 830  negantlem2 831  negantlem3 832  negantlem9 841  negantlem10 843  neg3antlem1 846  neg3antlem2 847  neg3ant1 848  elimconslem 849  elimcons 850  mhlem 858  mhlem2 860  marsdenlem3 864  marsdenlem4 865  mlaconjolem 867  mlaconjo 868  mhcor1 870  oago3.29 871  oago3.21x 872  cancellem 873  kb10iii 875  govar2 877  gomaex4 880  gomaex3h3 884  gomaex3h6 887  gomaex3h7 888  gomaex3h8 889  gomaex3lem4 897  oas 905  oat 907  oatr 908  oau 909  oaur 910  oal42 915  oa23 916  oa4lem1 917  oa4lem2 918  oa3to4lem1 925  oa3to4lem2 926  oa6to4h1 935  oa6to4h2 936  oa6to4h3 937  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa4btoc 946  oa3-u2lem 966  oa3-2to2s 970  oa3-1to5 973  d3oa 975  d4oa 976  oaliv 983  oalem1 985  oadist2a 987  oadist2b 988  oagen1 994  oagen2 996  mloa 998  oadistc0 1001  oadistc 1002  oadistd 1003  oa4cl 1007  axoa4a 1016  4oagen1 1021  4oadist 1023

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

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

metamath.org