Theorem lttri 11031

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

Hypotheses

Ref	Expression
lt.1	⊢ 𝐴 ∈ ℝ
lt.2	⊢ 𝐵 ∈ ℝ
lt.3	⊢ 𝐶 ∈ ℝ

Assertion

Ref	Expression
lttri	⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)

Proof of Theorem lttri

Step	Hyp	Ref	Expression
1		lt.1	. 2 ⊢ 𝐴 ∈ ℝ
2		lt.2	. 2 ⊢ 𝐵 ∈ ℝ
3		lt.3	. 2 ⊢ 𝐶 ∈ ℝ
4		lttr 10982	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5	1, 2, 3, 4	mp3an 1459	1 ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   < clt 10940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-pre-lttrn 10877

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945

This theorem is referenced by:  1lt3  12076  2lt4  12078  1lt4  12079  3lt5  12081  2lt5  12082  1lt5  12083  4lt6  12085  3lt6  12086  2lt6  12087  1lt6  12088  5lt7  12090  4lt7  12091  3lt7  12092  2lt7  12093  1lt7  12094  6lt8  12096  5lt8  12097  4lt8  12098  3lt8  12099  2lt8  12100  1lt8  12101  7lt9  12103  6lt9  12104  5lt9  12105  4lt9  12106  3lt9  12107  2lt9  12108  1lt9  12109  8lt10  12498  7lt10  12499  6lt10  12500  5lt10  12501  4lt10  12502  3lt10  12503  2lt10  12504  1lt10  12505  sincos2sgn  15831  epos  15844  ene1  15847  dvdslelem  15946  oppcbasOLD  17346  sralemOLD  20355  zlmlemOLD  20631  psgnodpmr  20707  tnglemOLD  23703  xrhmph  24016  vitalilem4  24680  pipos  25522  logneg  25648  asin1  25949  reasinsin  25951  atan1  25983  log2le1  26005  bposlem8  26344  bposlem9  26345  chebbnd1lem2  26523  chebbnd1lem3  26524  chebbnd1  26525  mulog2sumlem2  26588  pntibndlem1  26642  pntlemb  26650  pntlemk  26659  ttglemOLD  27142  cchhllemOLD  27158  axlowdimlem16  27228  dp2ltc  31063  sgnnbi  32412  sgnpbi  32413  signswch  32440  hgt750lem  32531  hgt750lem2  32532  logi  33606  cnndvlem1  34644  bj-minftyccb  35323  bj-pinftynminfty  35325  irrdiff  35424  asindmre  35787  fdc  35830  sn-0ne2  40310  fourierdlem94  43631  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem113  43650  fourierdlem114  43651  fouriersw  43662  etransclem23  43688