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

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

Proof of Theorem ltletrd
StepHypRef Expression
1 ltletrd.4 . 2 (𝜑𝐴 < 𝐵)
2 ltletrd.5 . 2 (𝜑𝐵𝐶)
3 ltd.1 . . 3 (𝜑𝐴 ∈ ℝ)
4 ltd.2 . . 3 (𝜑𝐵 ∈ ℝ)
5 letrd.3 . . 3 (𝜑𝐶 ∈ ℝ)
6 ltletr 9977 . . 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 4574  cr 9788   < clt 9927  cle 9928
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 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-resscn 9846  ax-pre-lttri 9863  ax-pre-lttrn 9864
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 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-er 7603  df-en 7816  df-dom 7817  df-sdom 7818  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933
This theorem is referenced by:  lelttrdi  10047  uzwo3  11612  rpgecl  11688  fznatpl1  12217  elfz1b  12231  modabs  12517  seqf1olem1  12654  expgt1  12712  leexp2a  12730  bernneq3  12806  expnbnd  12807  expmulnbnd  12810  digit1  12812  discr1  12814  hashfun  13033  seqcoll2  13055  abssubne0  13847  icodiamlt  13965  reccn2  14118  isercolllem1  14186  isumltss  14362  fprodntriv  14454  efcllem  14590  sin01bnd  14697  cos01bnd  14698  sin01gt0  14702  eirrlem  14714  rpnnen2lem11  14735  ruclem10  14750  bitsmod  14939  bitsinv1lem  14944  smuval2  14985  prmreclem5  15405  1arith  15412  2expltfac  15580  mndodconglem  17726  sylow1lem1  17779  gzrngunit  19574  nlmvscnlem1  22230  nrginvrcnlem  22235  iccpnfhmeo  22480  cnheibor  22490  evth  22494  lebnumlem1  22496  ipcnlem1  22767  lmnn  22784  ovolicc2lem2  23007  itg2monolem1  23237  itg2monolem3  23239  dvferm1lem  23465  dvcnvre  23500  dvfsumlem3  23509  dvfsumrlim  23512  plyco0  23666  aaliou2b  23814  pilem2  23924  cosordlem  23995  logdivlti  24084  logdivle  24086  logcnlem3  24104  logcnlem4  24105  cxpcn3lem  24202  atanre  24326  atanlogaddlem  24354  atans2  24372  ressatans  24375  birthdaylem3  24394  cxp2lim  24417  cxploglim2  24419  jensenlem2  24428  harmonicubnd  24450  fsumharmonic  24452  lgamgulmlem2  24470  lgamgulmlem3  24471  lgamucov  24478  ftalem2  24514  ftalem5  24517  vma1  24606  chtrpcl  24615  ppiltx  24617  fsumfldivdiaglem  24629  chtub  24651  fsumvma2  24653  chpval2  24657  chpchtsum  24658  chpub  24659  bpos1  24722  bposlem1  24723  bposlem2  24724  bposlem6  24728  gausslemma2dlem0c  24797  lgsquadlem1  24819  chebbnd1lem1  24872  chebbnd1lem2  24873  chebbnd1lem3  24874  chebbnd1  24875  chtppilimlem1  24876  chtppilimlem2  24877  chtppilim  24878  chto1ub  24879  chebbnd2  24880  chto1lb  24881  chpchtlim  24882  chpo1ub  24883  rplogsumlem2  24888  dchrisumlema  24891  dchrisumlem3  24894  dchrmusumlema  24896  dchrvmasumlem2  24901  dchrvmasumiflem1  24904  dchrisum0lema  24917  mulog2sumlem1  24937  chpdifbndlem1  24956  chpdifbnd  24958  pntrsumo1  24968  pntpbnd1  24989  pntpbnd2  24990  pntibndlem2  24994  pntlemb  25000  pntlemh  25002  pntlemr  25005  pntlem3  25012  pnt2  25016  ostth2lem1  25021  ostth2lem3  25038  ostth2lem4  25039  axsegconlem7  25518  axsegconlem10  25521  axlowdimlem16  25552  axcontlem2  25560  axcontlem4  25562  axcontlem7  25565  clwwlkn0  26065  clwlkisclwwlklem2a2  26071  clwwlkext2edg  26093  frgraregord013  26408  smatrcl  28993  1smat1  29001  lmdvg  29130  dya2icoseg  29469  eulerpartlems  29552  subfacval3  30228  knoppndvlem1  31476  knoppndvlem2  31477  knoppndvlem7  31482  knoppndvlem14  31489  knoppndvlem18  31493  poimirlem7  32386  poimirlem24  32403  poimirlem29  32408  mblfinlem2  32417  itg2addnclem  32431  itg2addnclem3  32433  ftc1anclem5  32459  ftc1anclem7  32461  ftc1anc  32463  areacirclem5  32474  irrapxlem4  36207  irrapxlem5  36208  pellexlem2  36212  pell14qrgapw  36258  pellqrex  36261  pellfundgt1  36265  pellfundex  36268  ltrmxnn0  36334  jm2.24nn  36344  jm2.17c  36347  jm2.24  36348  jm2.23  36381  jm3.1lem1  36402  jm3.1lem2  36403  radcnvrat  37335  dstregt0  38234  monoords  38252  fsumnncl  38439  mullimc  38484  mullimcf  38491  sumnnodd  38498  limcleqr  38512  addlimc  38516  0ellimcdiv  38517  limclner  38519  dvdivbd  38614  ioodvbdlimc1lem1  38622  ioodvbdlimc1lem2  38623  ioodvbdlimc2lem  38625  dvnmul  38634  iblspltprt  38666  itgspltprt  38672  stoweidlem11  38705  stoweidlem24  38718  stoweidlem25  38719  stoweidlem26  38720  stoweidlem34  38728  stoweidlem36  38730  stoweidlem42  38736  stoweidlem44  38738  stoweidlem51  38745  stoweidlem59  38753  wallispi  38764  wallispi2lem1  38765  wallispi2  38767  stirlinglem11  38778  dirkertrigeqlem1  38792  dirkeritg  38796  fourierdlem10  38811  fourierdlem11  38812  fourierdlem12  38813  fourierdlem15  38816  fourierdlem19  38820  fourierdlem20  38821  fourierdlem30  38831  fourierdlem32  38833  fourierdlem40  38841  fourierdlem41  38842  fourierdlem44  38845  fourierdlem46  38846  fourierdlem47  38847  fourierdlem48  38848  fourierdlem49  38849  fourierdlem50  38850  fourierdlem63  38863  fourierdlem64  38864  fourierdlem65  38865  fourierdlem74  38874  fourierdlem75  38875  fourierdlem76  38876  fourierdlem78  38878  fourierdlem79  38879  fourierdlem89  38889  fourierdlem92  38892  fourierdlem103  38903  fourierdlem104  38904  fouriersw  38925  etransclem4  38932  etransclem23  38951  etransclem31  38959  etransclem32  38960  etransclem35  38963  etransclem41  38969  etransclem48  38976  ioorrnopnlem  39001  sge0uzfsumgt  39138  sge0seq  39140  iundjiun  39154  carageniuncllem2  39213  hoidmvlelem3  39288  iunhoiioolem  39367  vonioolem1  39372  smfmullem1  39477  smfmullem2  39478  smfmullem3  39479  bgoldbtbndlem2  40024  clwlkclwwlklem2a2  41201  clwwlksext2edg  41229  logbpw2m1  42158
  Copyright terms: Public domain W3C validator