Theorem le3tr2 141

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 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 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

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