Theorem le3tr2 141

Description: Transitive inference useful for eliminating definitions. (Contributed by NM, 27-Aug-1997.)

Hypotheses

Ref	Expression
le3tr2.1	a ≤ b
le3tr2.2	a = c
le3tr2.3	b = d

Assertion

Ref	Expression
le3tr2	c ≤ d

Proof of Theorem le3tr2

Step	Hyp	Ref	Expression
1		le3tr2.1	. 2 a ≤ b
2		le3tr2.2	. . 3 a = c
3	2	ax-r1 35	. 2 c = a
4		le3tr2.3	. . 3 b = d
5	4	ax-r1 35	. 2 d = b
6	1, 3, 5	le3tr1 140	1 c ≤ d

Syntax hints:   = wb 1   ≤ wle 2

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

This theorem is referenced by:  ka4ot  435  3vded21  817  2oai1u  822  2oalem1  825  3vroa  831  mlaoml  833  sa5  836  neg3antlem2  865  elimconslem  867  elimcons  868  elimcons2  869  kb10iii  893  gomaex3lem6  919  oau  929  oa6v4v  933  oa4v3v  934  distoah2  941  distoah3  942  distoa  944  oa3to4lem6  950  oa6fromdualn  954  oa6to4  958  oa4to6  965  oa8to5  972  oa4to4u  973  oa3-2to2s  990  d3oa  995  mloa  1018  3oa2  1024  dp15lemc  1156  xdp15  1199  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208