Theorem le3tr2 133

Description: Transitive inference useful for eliminating definitions.

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 34	. 2 c = a
4		le3tr2.3	. . 3 b = d
5	4	ax-r1 34	. 2 d = b
6	1, 3, 5	le3tr1 132	1 c =< d

Syntax hints:   = wb 1   =< wle 2

This theorem is referenced by:  ka4ot 417  3vded21 799  2oai1u 804  2oalem1 807  3vroa 813  mlaoml 815  sa5 818  neg3antlem2 847  elimconslem 849  elimcons 850  elimcons2 851  kb10iii 875  gomaex3lem6 899  oau 909  oa6v4v 913  oa4v3v 914  distoah2 921  distoah3 922  distoa 924  oa3to4lem6 930  oa6fromdualn 934  oa6to4 938  oa4to6 945  oa8to5 952  oa4to4u 953  oa3-2to2s 970  d3oa 975  mloa 998  3oa2 1004

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