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

Theorem ltletrd 10157
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 10089 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1323 . 2 (𝜑 → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 714 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1987   class class class wbr 4623  cr 9895   < clt 10034  cle 10035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-resscn 9953  ax-pre-lttri 9970  ax-pre-lttrn 9971
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-mpt 4685  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-er 7702  df-en 7916  df-dom 7917  df-sdom 7918  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040
This theorem is referenced by:  lelttrdi  10159  uzwo3  11743  rpgecl  11819  fznatpl1  12353  elfz1b  12367  modabs  12659  seqf1olem1  12796  expgt1  12854  leexp2a  12872  bernneq3  12948  expnbnd  12949  expmulnbnd  12952  digit1  12954  discr1  12956  hashfun  13180  seqcoll2  13203  abssubne0  14006  icodiamlt  14124  reccn2  14277  isercolllem1  14345  isumltss  14524  fprodntriv  14616  efcllem  14752  sin01bnd  14859  cos01bnd  14860  sin01gt0  14864  eirrlem  14876  rpnnen2lem11  14897  ruclem10  14912  bitsmod  15101  bitsinv1lem  15106  smuval2  15147  prmreclem5  15567  1arith  15574  2expltfac  15742  mndodconglem  17900  sylow1lem1  17953  gzrngunit  19752  nlmvscnlem1  22430  nrginvrcnlem  22435  iccpnfhmeo  22684  cnheibor  22694  evth  22698  lebnumlem1  22700  ipcnlem1  22984  lmnn  23001  ovolicc2lem2  23226  itg2monolem1  23457  itg2monolem3  23459  dvferm1lem  23685  dvcnvre  23720  dvfsumlem3  23729  dvfsumrlim  23732  plyco0  23886  aaliou2b  24034  pilem2  24144  cosordlem  24215  logdivlti  24304  logdivle  24306  logcnlem3  24324  logcnlem4  24325  cxpcn3lem  24422  atanre  24546  atanlogaddlem  24574  atans2  24592  ressatans  24595  birthdaylem3  24614  cxp2lim  24637  cxploglim2  24639  jensenlem2  24648  harmonicubnd  24670  fsumharmonic  24672  lgamgulmlem2  24690  lgamgulmlem3  24691  lgamucov  24698  ftalem2  24734  ftalem5  24737  vma1  24826  chtrpcl  24835  ppiltx  24837  fsumfldivdiaglem  24849  chtub  24871  fsumvma2  24873  chpval2  24877  chpchtsum  24878  chpub  24879  bpos1  24942  bposlem1  24943  bposlem2  24944  bposlem6  24948  gausslemma2dlem0c  25017  lgsquadlem1  25039  chebbnd1lem1  25092  chebbnd1lem2  25093  chebbnd1lem3  25094  chebbnd1  25095  chtppilimlem1  25096  chtppilimlem2  25097  chtppilim  25098  chto1ub  25099  chebbnd2  25100  chto1lb  25101  chpchtlim  25102  chpo1ub  25103  rplogsumlem2  25108  dchrisumlema  25111  dchrisumlem3  25114  dchrmusumlema  25116  dchrvmasumlem2  25121  dchrvmasumiflem1  25124  dchrisum0lema  25137  mulog2sumlem1  25157  chpdifbndlem1  25176  chpdifbnd  25178  pntrsumo1  25188  pntpbnd1  25209  pntpbnd2  25210  pntibndlem2  25214  pntlemb  25220  pntlemh  25222  pntlemr  25225  pntlem3  25232  pnt2  25236  ostth2lem1  25241  ostth2lem3  25258  ostth2lem4  25259  axsegconlem7  25737  axsegconlem10  25740  axlowdimlem16  25771  axcontlem2  25779  axcontlem4  25781  axcontlem7  25784  clwlkclwwlklem2a2  26795  clwwlksext2edg  26823  smatrcl  29686  1smat1  29694  lmdvg  29823  dya2icoseg  30162  eulerpartlems  30245  subfacval3  30932  knoppndvlem1  32198  knoppndvlem2  32199  knoppndvlem7  32204  knoppndvlem14  32211  knoppndvlem18  32215  poimirlem7  33087  poimirlem24  33104  poimirlem29  33109  mblfinlem2  33118  itg2addnclem  33132  itg2addnclem3  33134  ftc1anclem5  33160  ftc1anclem7  33162  ftc1anc  33164  areacirclem5  33175  irrapxlem4  36908  irrapxlem5  36909  pellexlem2  36913  pell14qrgapw  36959  pellqrex  36962  pellfundgt1  36966  pellfundex  36969  ltrmxnn0  37035  jm2.24nn  37045  jm2.17c  37048  jm2.24  37049  jm2.23  37082  jm3.1lem1  37103  jm3.1lem2  37104  radcnvrat  38034  dstregt0  38992  monoords  39010  fsumnncl  39239  mullimc  39284  mullimcf  39291  sumnnodd  39298  limcleqr  39312  addlimc  39316  0ellimcdiv  39317  limclner  39319  dvdivbd  39475  ioodvbdlimc1lem1  39483  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvnmul  39495  iblspltprt  39526  itgspltprt  39532  stoweidlem11  39565  stoweidlem24  39578  stoweidlem25  39579  stoweidlem26  39580  stoweidlem34  39588  stoweidlem36  39590  stoweidlem42  39596  stoweidlem44  39598  stoweidlem51  39605  stoweidlem59  39613  wallispi  39624  wallispi2lem1  39625  wallispi2  39627  stirlinglem11  39638  dirkertrigeqlem1  39652  dirkeritg  39656  fourierdlem10  39671  fourierdlem11  39672  fourierdlem12  39673  fourierdlem15  39676  fourierdlem19  39680  fourierdlem20  39681  fourierdlem30  39691  fourierdlem32  39693  fourierdlem40  39701  fourierdlem41  39702  fourierdlem44  39705  fourierdlem46  39706  fourierdlem47  39707  fourierdlem48  39708  fourierdlem49  39709  fourierdlem50  39710  fourierdlem63  39723  fourierdlem64  39724  fourierdlem65  39725  fourierdlem74  39734  fourierdlem75  39735  fourierdlem76  39736  fourierdlem78  39738  fourierdlem79  39739  fourierdlem89  39749  fourierdlem92  39752  fourierdlem103  39763  fourierdlem104  39764  fouriersw  39785  etransclem4  39792  etransclem23  39811  etransclem31  39819  etransclem32  39820  etransclem35  39823  etransclem41  39829  etransclem48  39836  ioorrnopnlem  39861  sge0uzfsumgt  39998  sge0seq  40000  iundjiun  40014  carageniuncllem2  40073  hoidmvlelem3  40148  iunhoiioolem  40226  vonioolem1  40231  smfmullem1  40335  smfmullem2  40336  smfmullem3  40337  bgoldbtbndlem2  41013  logbpw2m1  41683
  Copyright terms: Public domain W3C validator