Theorem lttri 11384

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 11334	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5	1, 2, 3, 4	mp3an 1460	1 ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151   < clt 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-pre-lttrn 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297

This theorem is referenced by:  1lt3  12436  2lt4  12438  1lt4  12439  3lt5  12441  2lt5  12442  1lt5  12443  4lt6  12445  3lt6  12446  2lt6  12447  1lt6  12448  5lt7  12450  4lt7  12451  3lt7  12452  2lt7  12453  1lt7  12454  6lt8  12456  5lt8  12457  4lt8  12458  3lt8  12459  2lt8  12460  1lt8  12461  7lt9  12463  6lt9  12464  5lt9  12465  4lt9  12466  3lt9  12467  2lt9  12468  1lt9  12469  8lt10  12862  7lt10  12863  6lt10  12864  5lt10  12865  4lt10  12866  3lt10  12867  2lt10  12868  1lt10  12869  sincos2sgn  16226  epos  16239  ene1  16242  dvdslelem  16342  oppcbasOLD  17764  sralemOLD  21193  zlmlemOLD  21545  psgnodpmr  21625  tnglemOLD  24669  xrhmph  24991  vitalilem4  25659  pipos  26516  logi  26643  logneg  26644  asin1  26951  reasinsin  26953  atan1  26985  log2le1  27007  bposlem8  27349  bposlem9  27350  chebbnd1lem2  27528  chebbnd1lem3  27529  chebbnd1  27530  mulog2sumlem2  27593  pntibndlem1  27647  pntlemb  27655  pntlemk  27664  ttglemOLD  28900  cchhllemOLD  28916  axlowdimlem16  28986  dp2ltc  32853  sgnnbi  34526  sgnpbi  34527  signswch  34554  hgt750lem  34644  hgt750lem2  34645  cnndvlem1  36519  bj-minftyccb  37207  bj-pinftynminfty  37209  irrdiff  37308  asindmre  37689  fdc  37731  lttrii  42275  sn-0ne2  42412  fourierdlem94  46155  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem113  46174  fourierdlem114  46175  fouriersw  46186  etransclem23  46212