Theorem le3tr1 140

Description: Transitive inference useful for introducing definitions.

Hypotheses

Ref	Expression
le3tr1.1	a =< b
le3tr1.2	c = a
le3tr1.3	d = b

Assertion

Ref	Expression
le3tr1	c =< d

Proof of Theorem le3tr1

Step	Hyp	Ref	Expression
1		le3tr1.2	. . 3 c = a
2		le3tr1.1	. . 3 a =< b
3	1, 2	bltr 138	. 2 c =< b
4		le3tr1.3	. . 3 d = b
5	4	ax-r1 35	. 2 b = d
6	3, 5	lbtr 139	1 c =< d

Syntax hints:   = wb 1   =< wle 2

This theorem is referenced by:  le3tr2 141  lecon1 155  lelor 166  lelan 167  ledir 175  ledior 177  ka4lemo 228  ska13 241  i5lei1 347  i5lei2 348  i5lei3 349  i5lei4 350  id5leid0 351  wdf-c2 384  i3bi 496  i3th5 547  i3orlem5 556  ud4lem1a 577  u1lemc6 706  comi1 709  i2bi 722  u3lem14mp 794  3vth1 804  1oa 820  1oai1 821  mlalem 832  sa5 836  sadm3 838  bi3 839  negantlem2 849  negantlem3 850  negantlem9 859  negantlem10 861  neg3antlem2 865  comanb 872  mhlemlem2 875  mh 879  mlaconjo 886  cancellem 891  gomaex4 900  gomaex3h1 902  gomaex3h2 903  gomaex3h3 904  gomaex3h4 905  gomaex3h5 906  gomaex3h6 907  gomaex3h7 908  gomaex3h8 909  gomaex3h9 910  gomaex3h10 911  gomaex3h11 912  gomaex3h12 913  oa23 936  oa4lem1 937  oa4lem2 938  distoah4 943  oa3to4lem5 949  oa6todual 952  oa6fromdual 953  oa8todual 971  oal2 999  oal1 1000  lem3.3.3lem1 1048  lem3.3.3lem2 1049  lem3.3.5 1054  lem3.4.3 1075

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