Theorem lttri 10768

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   class class class wbr 5068  ℝcr 10538   < clt 10677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-pre-lttrn 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-ltxr 10682

This theorem is referenced by:  1lt3  11813  2lt4  11815  1lt4  11816  3lt5  11818  2lt5  11819  1lt5  11820  4lt6  11822  3lt6  11823  2lt6  11824  1lt6  11825  5lt7  11827  4lt7  11828  3lt7  11829  2lt7  11830  1lt7  11831  6lt8  11833  5lt8  11834  4lt8  11835  3lt8  11836  2lt8  11837  1lt8  11838  7lt9  11840  6lt9  11841  5lt9  11842  4lt9  11843  3lt9  11844  2lt9  11845  1lt9  11846  8lt10  12233  7lt10  12234  6lt10  12235  5lt10  12236  4lt10  12237  3lt10  12238  2lt10  12239  1lt10  12240  sincos2sgn  15549  epos  15562  ene1  15565  dvdslelem  15661  oppcbas  16990  sralem  19951  zlmlem  20666  psgnodpmr  20736  tnglem  23251  xrhmph  23553  vitalilem4  24214  pipos  25048  logneg  25173  asin1  25474  reasinsin  25476  atan1  25508  log2le1  25530  bposlem8  25869  bposlem9  25870  chebbnd1lem2  26048  chebbnd1lem3  26049  chebbnd1  26050  mulog2sumlem2  26113  pntibndlem1  26167  pntlemb  26175  pntlemk  26184  ttglem  26664  cchhllem  26675  axlowdimlem16  26745  dp2ltc  30565  sgnnbi  31805  sgnpbi  31806  signswch  31833  hgt750lem  31924  hgt750lem2  31925  logi  32968  cnndvlem1  33878  bj-minftyccb  34509  bj-pinftynminfty  34511  asindmre  34979  fdc  35022  sn-0ne2  39243  fourierdlem94  42492  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem112  42510  fourierdlem113  42511  fourierdlem114  42512  fouriersw  42523  etransclem23  42549