Theorem le3tr1 132

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 130	. 2 c ≤ b
4		le3tr1.3	. . 3 d = b
5	4	ax-r1 34	. 2 b = d
6	3, 5	lbtr 131	1 c ≤ d

Syntax hints:   = wb 1   ≤ wle 2

This theorem is referenced by:  le3tr2 133  lecon1 147  lelor 158  lelan 159  ledir 167  ledior 169  ka4lemo 220  ska13 233  i5lei1 339  i5lei2 340  i5lei3 341  i5lei4 342  wdf-c2 366  i3bi 478  i3th5 529  i3orlem5 538  ud4lem1a 559  u1lemc6 688  comi1 691  i2bi 704  u3lem14mp 776  3vth1 786  1oa 802  1oai1 803  mlalem 814  sa5 818  sadm3 820  bi3 821  negantlem2 831  negantlem3 832  negantlem9 841  negantlem10 843  neg3antlem2 847  comanb 854  mhlemlem2 857  mh 861  mlaconjo 868  cancellem 873  gomaex4 880  gomaex3h1 882  gomaex3h2 883  gomaex3h3 884  gomaex3h4 885  gomaex3h5 886  gomaex3h6 887  gomaex3h7 888  gomaex3h8 889  gomaex3h9 890  gomaex3h10 891  gomaex3h11 892  gomaex3h12 893  oa23 916  oa4lem1 917  oa4lem2 918  distoah4 923  oa3to4lem5 929  oa6todual 932  oa6fromdual 933  oa8todual 951  oal2 979  oal1 980

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