Theorem lttri 11466

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   class class class wbr 5106  ℝcr 11229   < clt 11373

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-resscn 11287  ax-pre-lttrn 11305

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-ltxr 11378

This theorem is used by:  1lt3  12548  2lt4  12550  1lt4  12551  3lt5  12553  2lt5  12554  1lt5  12555  4lt6  12557  3lt6  12558  2lt6  12559  1lt6  12560  5lt7  12562  4lt7  12563  3lt7  12564  2lt7  12565  1lt7  12566  6lt8  12568  5lt8  12569  4lt8  12570  3lt8  12571  2lt8  12572  1lt8  12573  7lt9  12575  6lt9  12576  5lt9  12577  4lt9  12578  3lt9  12579  2lt9  12580  1lt9  12581  1lt10OLD  12990  sgnnbi  15289  sgnpbi  15290  sincos2sgn  16394  epos  16407  ene1  16410  dvdslelem  16511  psgnodpmr  21929  xrhmph  25301  vitalilem4  25965  pipos  26820  logi  26948  logneg  26949  asin1  27255  reasinsin  27257  atan1  27289  log2le1  27311  bposlem8  27651  bposlem9  27652  chebbnd1lem2  27830  chebbnd1lem3  27831  chebbnd1  27832  mulog2sumlem2  27895  pntibndlem1  27949  pntlemb  27957  pntlemk  27966  axlowdimlem16  29568  dp2ltc  33526  signswch  35273  hgt750lem  35363  hgt750lem2  35364  cnndvlem1  37594  bj-minftyccb  38351  bj-pinftynminfty  38353  irrdiff  38452  asindmre  38826  fdc  38882  lttrii  43510  sn-0ne2  43661  fourierdlem94  47425  fourierdlem102  47433  fourierdlem103  47434  fourierdlem104  47435  fourierdlem112  47443  fourierdlem113  47444  fourierdlem114  47445  fouriersw  47456  etransclem23  47482  goldrapos  48145