Theorem le3tr1 140

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

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

This proof depends on syntax axioms:   = wb 1   ≤ wle 2

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-a 40  df-le1 130  df-le2 131

This theorem is used 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  oa3moa3  1029  lem3.3.3lem1  1049  lem3.3.3lem2  1050  lem3.3.5  1055  lem3.4.3  1076