Theorem lttri 11307

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074   < clt 11215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220

This theorem is referenced by:  1lt3  12361  2lt4  12363  1lt4  12364  3lt5  12366  2lt5  12367  1lt5  12368  4lt6  12370  3lt6  12371  2lt6  12372  1lt6  12373  5lt7  12375  4lt7  12376  3lt7  12377  2lt7  12378  1lt7  12379  6lt8  12381  5lt8  12382  4lt8  12383  3lt8  12384  2lt8  12385  1lt8  12386  7lt9  12388  6lt9  12389  5lt9  12390  4lt9  12391  3lt9  12392  2lt9  12393  1lt9  12394  8lt10  12788  7lt10  12789  6lt10  12790  5lt10  12791  4lt10  12792  3lt10  12793  2lt10  12794  1lt10  12795  sincos2sgn  16169  epos  16182  ene1  16185  dvdslelem  16286  psgnodpmr  21506  xrhmph  24852  vitalilem4  25519  pipos  26375  logi  26503  logneg  26504  asin1  26811  reasinsin  26813  atan1  26845  log2le1  26867  bposlem8  27209  bposlem9  27210  chebbnd1lem2  27388  chebbnd1lem3  27389  chebbnd1  27390  mulog2sumlem2  27453  pntibndlem1  27507  pntlemb  27515  pntlemk  27524  axlowdimlem16  28891  sgnnbi  32770  sgnpbi  32771  dp2ltc  32814  signswch  34559  hgt750lem  34649  hgt750lem2  34650  cnndvlem1  36532  bj-minftyccb  37220  bj-pinftynminfty  37222  irrdiff  37321  asindmre  37704  fdc  37746  lttrii  42251  sn-0ne2  42401  fourierdlem94  46205  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem113  46224  fourierdlem114  46225  fouriersw  46236  etransclem23  46262