Theorem lbtr 139

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 35	. . . 4 c = b
3	2	lan 77	. . 3 (a ^ c) = (a ^ b)
4		lbtr.1	. . . 4 a =< b
5	4	df2le2 136	. . 3 (a ^ b) = a
6	3, 5	ax-r2 36	. 2 (a ^ c) = a
7	6	df2le1 135	1 a =< c

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

This theorem is referenced by:  le3tr1 140  lerr 150  lecon2 156  leor 159  lel2or 170  lel2an 171  ledi 174  ledio 176  ka4lemo 228  wlem1 243  ska15 244  bina4 285  bina5 286  womle2b 296  womle3b 297  nom14 311  nom20 313  nom23 316  nom24 317  go1 343  i2or 344  i1or 345  k1-8a 355  k1-8b 356  wom2 434  ka4ot 435  ortha 438  i3bi 496  lem4 511  binr3 519  i3th5 547  i3th7 549  i3th8 550  i3orlem1 552  i3orlem4 555  i3orlem7 558  i3orlem8 559  ud3lem1c 568  ud4lem1c 579  u1lemc6 706  i2bi 722  u12lembi 726  u1lem9b 778  u3lem14mp 794  3vth6 809  3vded11 814  3vded12 815  3vded21 817  3vded22 818  oaeqv 830  sadm3 838  bi3 839  bi4 840  mlaconj4 844  mlaconj 845  negantlem1 848  negantlem2 849  negantlem3 850  negantlem9 859  negantlem10 861  neg3antlem1 864  neg3antlem2 865  neg3ant1 866  elimconslem 867  elimcons 868  mhlem 876  mhlem2 878  marsdenlem3 882  marsdenlem4 883  mlaconjolem 885  mlaconjo 886  mhcor1 888  oago3.29 889  oago3.21x 890  cancellem 891  kb10iii 893  e2ast2 894  govar2 897  gomaex4 900  gomaex3h3 904  gomaex3h6 907  gomaex3h7 908  gomaex3h8 909  gomaex3lem4 917  oas 925  oat 927  oatr 928  oau 929  oaur 930  oal42 935  oa23 936  oa4lem1 937  oa4lem2 938  oa3to4lem1 945  oa3to4lem2 946  oa6to4h1 955  oa6to4h2 956  oa6to4h3 957  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  oa4btoc 966  oa3-u2lem 986  oa3-2to2s 990  oa3-1to5 993  d3oa 995  d4oa 996  oaliv 1003  oalem1 1005  oadist2a 1007  oadist2b 1008  oagen1 1014  oagen2 1016  mloa 1018  oadistc0 1021  oadistc 1022  oadistd 1023  oa4cl 1027  axoa4a 1036  4oagen1 1041  4oadist 1043  lem3.3.5 1054  lem3.4.3 1075  lem4.6.7 1100

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

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

Copyright terms: Public domain