Theorem lttri 11364

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   class class class wbr 5107  ℝcr 11127   < clt 11271

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-resscn 11185  ax-pre-lttrn 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-ltxr 11276

This theorem is used by:  1lt3  12444  2lt4  12446  1lt4  12447  3lt5  12449  2lt5  12450  1lt5  12451  4lt6  12453  3lt6  12454  2lt6  12455  1lt6  12456  5lt7  12458  4lt7  12459  3lt7  12460  2lt7  12461  1lt7  12462  6lt8  12464  5lt8  12465  4lt8  12466  3lt8  12467  2lt8  12468  1lt8  12469  7lt9  12471  6lt9  12472  5lt9  12473  4lt9  12474  3lt9  12475  2lt9  12476  1lt9  12477  1lt10OLD  12886  sgnnbi  15181  sgnpbi  15182  sincos2sgn  16288  epos  16301  ene1  16304  dvdslelem  16405  psgnodpmr  21809  xrhmph  25181  vitalilem4  25845  pipos  26703  logi  26832  logneg  26833  asin1  27139  reasinsin  27141  atan1  27173  log2le1  27195  bposlem8  27535  bposlem9  27536  chebbnd1lem2  27714  chebbnd1lem3  27715  chebbnd1  27716  mulog2sumlem2  27779  pntibndlem1  27833  pntlemb  27841  pntlemk  27850  axlowdimlem16  29422  dp2ltc  33340  signswch  35077  hgt750lem  35167  hgt750lem2  35168  cnndvlem1  37242  bj-minftyccb  37985  bj-pinftynminfty  37987  irrdiff  38086  asindmre  38460  fdc  38503  lttrii  43130  sn-0ne2  43289  fourierdlem94  47036  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem112  47054  fourierdlem113  47055  fourierdlem114  47056  fouriersw  47067  etransclem23  47093  goldrapos  47756