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

Theorem lttrd 10049
Description: Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.)
Hypotheses
Ref Expression
ltd.1 (𝜑𝐴 ∈ ℝ)
ltd.2 (𝜑𝐵 ∈ ℝ)
letrd.3 (𝜑𝐶 ∈ ℝ)
lttrd.4 (𝜑𝐴 < 𝐵)
lttrd.5 (𝜑𝐵 < 𝐶)
Assertion
Ref Expression
lttrd (𝜑𝐴 < 𝐶)

Proof of Theorem lttrd
StepHypRef Expression
1 lttrd.4 . 2 (𝜑𝐴 < 𝐵)
2 lttrd.5 . 2 (𝜑𝐵 < 𝐶)
3 ltd.1 . . 3 (𝜑𝐴 ∈ ℝ)
4 ltd.2 . . 3 (𝜑𝐵 ∈ ℝ)
5 letrd.3 . . 3 (𝜑𝐶 ∈ ℝ)
6 lttr 9965 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1317 . 2 (𝜑 → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 710 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976   class class class wbr 4577  cr 9791   < clt 9930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-pre-lttrn 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-ltxr 9935
This theorem is referenced by:  expgt1  12715  ltexp2a  12729  expcan  12730  ltexp2  12731  leexp2  12732  expnlbnd2  12812  expmulnbnd  12813  reccn2  14121  efgt1  14631  tanhlt1  14675  ruclem2  14746  isprm7  15204  pythagtriplem13  15316  fldivp1  15385  4sqlem12  15444  sylow1lem1  17782  telgsums  18159  chfacffsupp  20422  chfacfscmul0  20424  chfacfpmmul0  20428  nrginvrcnlem  22238  iccntr  22364  icccmplem2  22366  opnreen  22374  pjthlem1  22933  pmltpclem2  22942  ovollb2lem  22980  opnmbllem  23092  volivth  23098  lhop1lem  23497  dvcnvrelem1  23501  dvcvx  23504  ftc1lem4  23523  aaliou3lem7  23825  ulmdvlem1  23875  reeff1olem  23921  pilem2  23927  pilem3  23928  tangtx  23978  tanord1  24004  tanord  24005  rplogcl  24071  logimul  24081  logcnlem3  24107  efopnlem1  24119  cxplt  24157  cxple  24158  cxpcn3lem  24205  asinsin  24336  atanlogaddlem  24357  atanlogsublem  24359  cxp2limlem  24419  cxp2lim  24420  zetacvg  24458  lgamucov  24481  lgamcvg2  24498  ftalem1  24516  mersenne  24669  bposlem2  24727  bposlem6  24731  bposlem9  24734  lgsqrlem2  24789  lgsquadlem2  24823  chebbnd1lem2  24876  chebbnd1lem3  24877  chebbnd1  24878  chtppilimlem1  24879  chto1ub  24882  mulog2sumlem2  24941  chpdifbndlem1  24959  selberg3lem1  24963  pntrlog2bndlem2  24984  pntrlog2bndlem4  24986  pntpbnd1a  24991  pntpbnd1  24992  pntpbnd2  24993  pntibndlem1  24995  pntibndlem2  24997  pntibndlem3  24998  pntibnd  24999  pntlemb  25003  pntlemr  25008  pntlemf  25011  pnt  25020  ostth2lem1  25024  ostth2lem3  25041  ostth2lem4  25042  wwlkext2clwwlk  26097  eupap1  26269  frgraogt3nreg  26413  friendshipgt3  26414  pjhthlem1  27440  psgnfzto1stlem  28987  1smat1  29004  sqsscirc1  29088  xrge0iifiso  29115  sgnsub  29739  signslema  29771  knoppndvlem12  31490  knoppndvlem14  31492  knoppndvlem15  31493  knoppndvlem17  31495  knoppndvlem20  31498  poimirlem6  32381  poimirlem7  32382  poimirlem8  32383  poimirlem15  32390  poimirlem20  32395  poimirlem28  32403  opnmbllem0  32411  itg2gt0cn  32431  ftc1cnnclem  32449  ftc1anc  32459  cntotbnd  32561  pellexlem5  36211  pellfundex  36264  pellfundrp  36266  rmspecfund  36288  monotuz  36320  jm3.1lem2  36399  jm3.1lem3  36400  imo72b2  37293  prmunb2  37328  neglt  38233  ltadd12dd  38297  infleinflem2  38325  sqrlearg  38424  lptre2pt  38504  0ellimcdiv  38513  ioodvbdlimc1lem1  38618  iblspltprt  38662  itgspltprt  38668  stoweidlem7  38697  stoweidlem11  38701  stoweidlem13  38703  stoweidlem14  38704  stoweidlem26  38716  stoweidlem42  38732  stoweidlem52  38742  stoweidlem59  38749  stoweidlem60  38750  stoweidlem62  38752  wallispilem4  38758  wallispi  38760  stirlinglem1  38764  stirlinglem3  38766  stirlinglem6  38769  stirlinglem7  38770  stirlinglem10  38773  stirlinglem11  38774  dirkercncflem1  38793  dirkercncflem2  38794  fourierdlem10  38807  fourierdlem11  38808  fourierdlem12  38809  fourierdlem42  38839  fourierdlem47  38843  fourierdlem50  38846  fourierdlem51  38847  fourierdlem73  38869  fourierdlem79  38875  fourierdlem83  38879  fourierdlem103  38899  fourierdlem104  38900  sqwvfoura  38918  sqwvfourb  38919  fouriersw  38921  hoidmvlelem1  39282  hoiqssbllem2  39310  hspmbllem1  39313  pimrecltpos  39393  pimrecltneg  39407  smfaddlem1  39446  smflimlem3  39456  smflimlem4  39457  smfmullem1  39473  wwlksext2clwwlk  41226  av-frgraogt3nreg  41546  av-friendshipgt3  41547
  Copyright terms: Public domain W3C validator