Theorem lttri 11270

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   class class class wbr 5079  ℝcr 11035   < clt 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-pre-lttrn 11111

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182

This theorem is referenced by:  1lt3  12347  2lt4  12349  1lt4  12350  3lt5  12352  2lt5  12353  1lt5  12354  4lt6  12356  3lt6  12357  2lt6  12358  1lt6  12359  5lt7  12361  4lt7  12362  3lt7  12363  2lt7  12364  1lt7  12365  6lt8  12367  5lt8  12368  4lt8  12369  3lt8  12370  2lt8  12371  1lt8  12372  7lt9  12374  6lt9  12375  5lt9  12376  4lt9  12377  3lt9  12378  2lt9  12379  1lt9  12380  8lt10  12774  7lt10  12775  6lt10  12776  5lt10  12777  4lt10  12778  3lt10  12779  2lt10  12780  1lt10  12781  sincos2sgn  16159  epos  16172  ene1  16175  dvdslelem  16276  psgnodpmr  21572  xrhmph  24939  vitalilem4  25603  pipos  26448  logi  26576  logneg  26577  asin1  26883  reasinsin  26885  atan1  26917  log2le1  26939  bposlem8  27279  bposlem9  27280  chebbnd1lem2  27458  chebbnd1lem3  27459  chebbnd1  27460  mulog2sumlem2  27523  pntibndlem1  27577  pntlemb  27585  pntlemk  27594  axlowdimlem16  29051  sgnnbi  32937  sgnpbi  32938  dp2ltc  32972  signswch  34752  hgt750lem  34842  hgt750lem2  34843  cnndvlem1  36850  bj-minftyccb  37592  bj-pinftynminfty  37594  irrdiff  37693  asindmre  38077  fdc  38119  lttrii  42746  sn-0ne2  42890  fourierdlem94  46650  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fourierdlem113  46669  fourierdlem114  46670  fouriersw  46681  etransclem23  46707  goldrapos  47353