Theorem lttri 11324

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145   class class class wbr 5104  ℝcr 11087   < clt 11231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-resscn 11145  ax-pre-lttrn 11163

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-ltxr 11236

This theorem is referenced by:  1lt3  12404  2lt4  12406  1lt4  12407  3lt5  12409  2lt5  12410  1lt5  12411  4lt6  12413  3lt6  12414  2lt6  12415  1lt6  12416  5lt7  12418  4lt7  12419  3lt7  12420  2lt7  12421  1lt7  12422  6lt8  12424  5lt8  12425  4lt8  12426  3lt8  12427  2lt8  12428  1lt8  12429  7lt9  12431  6lt9  12432  5lt9  12433  4lt9  12434  3lt9  12435  2lt9  12436  1lt9  12437  1lt10OLD  12845  sgnnbi  15129  sgnpbi  15130  sincos2sgn  16238  epos  16251  ene1  16254  dvdslelem  16355  psgnodpmr  21697  xrhmph  25063  vitalilem4  25727  pipos  26577  logi  26706  logneg  26707  asin1  27013  reasinsin  27015  atan1  27047  log2le1  27069  bposlem8  27409  bposlem9  27410  chebbnd1lem2  27588  chebbnd1lem3  27589  chebbnd1  27590  mulog2sumlem2  27653  pntibndlem1  27707  pntlemb  27715  pntlemk  27724  axlowdimlem16  29212  dp2ltc  33114  signswch  34860  hgt750lem  34950  hgt750lem2  34951  cnndvlem1  36983  bj-minftyccb  37724  bj-pinftynminfty  37726  irrdiff  37825  asindmre  38209  fdc  38251  lttrii  42878  sn-0ne2  43022  fourierdlem94  46773  fourierdlem102  46781  fourierdlem103  46782  fourierdlem104  46783  fourierdlem112  46791  fourierdlem113  46792  fourierdlem114  46793  fouriersw  46804  etransclem23  46830  goldrapos  47476