Theorem lttri 10504

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107   class class class wbr 4888  ℝcr 10273   < clt 10413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-resscn 10331  ax-pre-lttrn 10349

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-pnf 10415  df-mnf 10416  df-ltxr 10418

This theorem is referenced by:  1lt3  11559  2lt4  11561  1lt4  11562  3lt5  11564  2lt5  11565  1lt5  11566  4lt6  11568  3lt6  11569  2lt6  11570  1lt6  11571  5lt7  11573  4lt7  11574  3lt7  11575  2lt7  11576  1lt7  11577  6lt8  11579  5lt8  11580  4lt8  11581  3lt8  11582  2lt8  11583  1lt8  11584  7lt9  11586  6lt9  11587  5lt9  11588  4lt9  11589  3lt9  11590  2lt9  11591  1lt9  11592  8lt10  11983  7lt10  11984  6lt10  11985  5lt10  11986  4lt10  11987  3lt10  11988  2lt10  11989  1lt10  11990  sincos2sgn  15330  epos  15343  ene1  15346  dvdslelem  15442  oppcbas  16767  sralem  19578  zlmlem  20265  psgnodpmr  20335  tnglem  22856  xrhmph  23158  vitalilem4  23819  pipos  24654  logneg  24775  asin1  25076  reasinsin  25078  atan1  25110  log2le1  25133  bposlem8  25472  bposlem9  25473  chebbnd1lem2  25615  chebbnd1lem3  25616  chebbnd1  25617  mulog2sumlem2  25680  pntibndlem1  25734  pntlemb  25742  pntlemk  25751  ttglem  26229  cchhllem  26240  axlowdimlem16  26310  dp2ltc  30161  sgnnbi  31210  sgnpbi  31211  signswch  31242  hgt750lem  31335  hgt750lem2  31336  logi  32218  cnndvlem1  33114  bj-minftyccb  33706  bj-pinftynminfty  33708  asindmre  34125  fdc  34170  fourierdlem94  41354  fourierdlem102  41362  fourierdlem103  41363  fourierdlem104  41364  fourierdlem112  41372  fourierdlem113  41373  fourierdlem114  41374  fouriersw  41385  etransclem23  41411