MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lttri Structured version   Visualization version   GIF version

Theorem lttri 10201
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
StepHypRef Expression
1 lt.1 . 2 𝐴 ∈ ℝ
2 lt.2 . 2 𝐵 ∈ ℝ
3 lt.3 . 2 𝐶 ∈ ℝ
4 lttr 10152 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
51, 2, 3, 4mp3an 1464 1 ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030   class class class wbr 4685  cr 9973   < clt 10112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-pre-lttrn 10049
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-ltxr 10117
This theorem is referenced by:  1lt3  11234  2lt4  11236  1lt4  11237  3lt5  11239  2lt5  11240  1lt5  11241  4lt6  11243  3lt6  11244  2lt6  11245  1lt6  11246  5lt7  11248  4lt7  11249  3lt7  11250  2lt7  11251  1lt7  11252  6lt8  11254  5lt8  11255  4lt8  11256  3lt8  11257  2lt8  11258  1lt8  11259  7lt9  11261  6lt9  11262  5lt9  11263  4lt9  11264  3lt9  11265  2lt9  11266  1lt9  11267  8lt10OLD  11269  7lt10OLD  11270  6lt10OLD  11271  5lt10OLD  11272  4lt10OLD  11273  3lt10OLD  11274  2lt10OLD  11275  1lt10OLD  11276  8lt10  11712  7lt10  11713  6lt10  11714  5lt10  11715  4lt10  11716  3lt10  11717  2lt10  11718  1lt10  11719  sincos2sgn  14968  epos  14979  ene1  14982  dvdslelem  15078  oppcbas  16425  sralem  19225  zlmlem  19913  psgnodpmr  19984  tnglem  22491  xrhmph  22793  vitalilem4  23425  pipos  24257  logneg  24379  asin1  24666  reasinsin  24668  atan1  24700  log2le1  24722  bposlem8  25061  bposlem9  25062  chebbnd1lem2  25204  chebbnd1lem3  25205  chebbnd1  25206  mulog2sumlem2  25269  pntibndlem1  25323  pntlemb  25331  pntlemk  25340  ttglem  25801  cchhllem  25812  axlowdimlem16  25882  dp2ltc  29722  sgnnbi  30735  sgnpbi  30736  signswch  30766  hgt750lem  30857  hgt750lem2  30858  logi  31746  cnndvlem1  32653  bj-minftyccb  33242  bj-pinftynminfty  33244  asindmre  33625  fdc  33671  fourierdlem94  40735  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  fourierdlem113  40754  fourierdlem114  40755  fouriersw  40766  etransclem23  40792
  Copyright terms: Public domain W3C validator