Theorem lttri 9615

Description: 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)

Hypotheses

Ref	Expression
lt.1	|- A e. RR
lt.2	|- B e. RR
lt.3	|- C e. RR

Assertion

Ref	Expression
lttri	|- ( ( A < B /\ B < C ) -> A < C )

Proof of Theorem lttri

Step	Hyp	Ref	Expression
1		lt.1	. 2 |- A e. RR
2		lt.2	. 2 |- B e. RR
3		lt.3	. 2 |- C e. RR
4		lttr 9566	. 2 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
5	1, 2, 3, 4	mp3an 1315	1 |- ( ( A < B /\ B < C ) -> A < C )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1758   class class class wbr 4403   RRcr 9396   < clt 9533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485  ax-resscn 9454  ax-pre-lttrn 9472

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-er 7214  df-en 7424  df-dom 7425  df-sdom 7426  df-pnf 9535  df-mnf 9536  df-ltxr 9538

This theorem is referenced by:  1lt3  10605  2lt4  10607  1lt4  10608  3lt5  10610  2lt5  10611  1lt5  10612  4lt6  10614  3lt6  10615  2lt6  10616  1lt6  10617  5lt7  10619  4lt7  10620  3lt7  10621  2lt7  10622  1lt7  10623  6lt8  10625  5lt8  10626  4lt8  10627  3lt8  10628  2lt8  10629  1lt8  10630  7lt9  10632  6lt9  10633  5lt9  10634  4lt9  10635  3lt9  10636  2lt9  10637  1lt9  10638  8lt10  10640  7lt10  10641  6lt10  10642  5lt10  10643  4lt10  10644  3lt10  10645  2lt10  10646  1lt10  10647  sincos2sgn  13600  epos  13611  dvdslelem  13699  oppcbas  14780  sralem  17391  zlmlem  18083  psgnodpmr  18155  tnglem  20368  xrhmph  20661  vitalilem4  21234  pipos  22066  logneg  22179  asin1  22432  reasinsin  22434  atan1  22466  bposlem8  22773  bposlem9  22774  chebbnd1lem2  22862  chebbnd1lem3  22863  chebbnd1  22864  mulog2sumlem2  22927  pntibndlem1  22981  pntlemb  22989  pntlemk  22998  ttglem  23301  cchhllem  23312  axlowdimlem16  23382  log2le1  26634  sgnnbi  27095  sgnpbi  27096  signswch  27129  asindmre  28650  fdc  28812  ene1  31460  bj-minftyccb  32911  bj-pinftynminfty  32913