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

Theorem ltletrd 11316
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 11248 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1372 . 2 (𝜑 → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 698 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107   class class class wbr 5106  cr 11051   < clt 11190  cle 11191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-pre-lttri 11126  ax-pre-lttrn 11127
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196
This theorem is referenced by:  lelttrdi  11318  uzwo3  12869  rpgecl  12944  fznatpl1  13496  modabs  13810  seqf1olem1  13948  expgt1  14007  leexp2a  14078  bernneq3  14135  expnbnd  14136  expmulnbnd  14139  digit1  14141  discr1  14143  hashfun  14338  seqcoll2  14365  abssubne0  15202  icodiamlt  15321  reccn2  15480  isercolllem1  15550  isumltss  15734  fprodntriv  15826  efcllem  15961  sin01bnd  16068  cos01bnd  16069  sin01gt0  16073  eirrlem  16087  rpnnen2lem11  16107  ruclem10  16122  bitsmod  16317  bitsinv1lem  16322  smuval2  16363  prmreclem5  16793  1arith  16800  2expltfac  16966  mndodconglem  19324  sylow1lem1  19381  gzrngunit  20866  nlmvscnlem1  24053  nrginvrcnlem  24058  iccpnfhmeo  24311  cnheibor  24321  evth  24325  lebnumlem1  24327  ipcnlem1  24612  lmnn  24630  ovolicc2lem2  24885  itg2monolem1  25118  itg2monolem3  25120  dvferm1lem  25351  dvcnvre  25386  dvfsumlem3  25395  dvfsumrlim  25398  plyco0  25556  aaliou2b  25704  pilem2  25814  cosq34lt1  25886  cosordlem  25889  logdivlti  25978  logdivle  25980  logcnlem3  26002  logcnlem4  26003  cxpcn3lem  26103  atanre  26238  atanlogaddlem  26266  atans2  26284  birthdaylem3  26306  cxp2lim  26329  cxploglim2  26331  jensenlem2  26340  harmonicubnd  26362  fsumharmonic  26364  lgamgulmlem2  26382  lgamgulmlem3  26383  lgamucov  26390  ftalem2  26426  ftalem5  26429  vma1  26518  chtrpcl  26527  ppiltx  26529  fsumfldivdiaglem  26541  chtub  26563  fsumvma2  26565  chpval2  26569  chpchtsum  26570  chpub  26571  bpos1  26634  bposlem1  26635  bposlem2  26636  bposlem6  26640  gausslemma2dlem0c  26709  lgsquadlem1  26731  chebbnd1lem1  26820  chebbnd1lem2  26821  chebbnd1lem3  26822  chebbnd1  26823  chtppilimlem1  26824  chtppilimlem2  26825  chtppilim  26826  chto1ub  26827  chebbnd2  26828  chto1lb  26829  chpchtlim  26830  chpo1ub  26831  rplogsumlem2  26836  dchrisumlema  26839  dchrisumlem3  26842  dchrmusumlema  26844  dchrvmasumlem2  26849  dchrvmasumiflem1  26852  dchrisum0lema  26865  mulog2sumlem1  26885  chpdifbndlem1  26904  chpdifbnd  26906  pntrsumo1  26916  pntpbnd1  26937  pntpbnd2  26938  pntibndlem2  26942  pntlemb  26948  pntlemh  26950  pntlemr  26953  pntlem3  26960  pnt2  26964  ostth2lem1  26969  ostth2lem3  26986  ostth2lem4  26987  axsegconlem7  27875  axsegconlem10  27878  axlowdimlem16  27909  axcontlem2  27917  axcontlem4  27919  axcontlem7  27922  clwlkclwwlklem2a2  28940  clwwlkext2edg  29003  smatrcl  32380  1smat1  32388  lmdvg  32537  dya2icoseg  32880  eulerpartlems  32963  reprlt  33235  reprinfz1  33238  breprexplemc  33248  hgt750lemd  33264  hgt750lem  33267  hgt750leme  33274  tgoldbachgtde  33276  subfacval3  33786  knoppndvlem1  34978  knoppndvlem2  34979  knoppndvlem7  34984  knoppndvlem14  34991  knoppndvlem18  34995  poimirlem7  36088  poimirlem24  36105  poimirlem29  36110  mblfinlem2  36119  itg2addnclem  36132  itg2addnclem3  36134  ftc1anclem5  36158  ftc1anclem7  36160  ftc1anc  36162  areacirclem5  36173  lcmineqlem23  40511  3lexlogpow5ineq2  40515  3lexlogpow5ineq4  40516  3lexlogpow5ineq3  40517  aks4d1lem1  40522  dvrelog2  40524  aks4d1p1p3  40529  aks4d1p1p2  40530  aks4d1p1p4  40531  aks4d1p1p6  40533  aks4d1p1p7  40534  aks4d1p1p5  40535  aks4d1p1  40536  aks4d1p2  40537  aks4d1p3  40538  aks4d1p5  40540  aks4d1p6  40541  aks4d1p7d1  40542  aks4d1p7  40543  aks4d1p8d2  40545  aks4d1p8  40547  aks4d1p9  40548  2ap1caineq  40556  sticksstones12a  40568  sticksstones22  40579  metakunt6  40585  metakunt11  40590  metakunt27  40606  metakunt28  40607  flt4lem7  41000  3cubeslem1  41010  irrapxlem4  41151  irrapxlem5  41152  pellexlem2  41156  pell14qrgapw  41202  pellqrex  41205  pellfundgt1  41209  pellfundex  41212  ltrmxnn0  41276  jm2.24nn  41286  jm2.17c  41289  jm2.24  41290  jm2.23  41323  jm3.1lem1  41344  jm3.1lem2  41345  radcnvrat  42601  dstregt0  43522  monoords  43538  uzubioo  43812  fsumnncl  43820  mullimc  43864  mullimcf  43871  sumnnodd  43878  limcleqr  43892  addlimc  43896  0ellimcdiv  43897  limclner  43899  limsupgtlem  44025  dvdivbd  44171  ioodvbdlimc1lem1  44179  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  dvnmul  44191  iblspltprt  44221  itgspltprt  44227  stoweidlem11  44259  stoweidlem24  44272  stoweidlem25  44273  stoweidlem26  44274  stoweidlem34  44282  stoweidlem36  44284  stoweidlem42  44290  stoweidlem44  44292  stoweidlem51  44299  stoweidlem59  44307  wallispi  44318  wallispi2lem1  44319  wallispi2  44321  stirlinglem11  44332  dirkertrigeqlem1  44346  dirkeritg  44350  fourierdlem10  44365  fourierdlem11  44366  fourierdlem12  44367  fourierdlem15  44370  fourierdlem19  44374  fourierdlem20  44375  fourierdlem30  44385  fourierdlem32  44387  fourierdlem40  44395  fourierdlem41  44396  fourierdlem44  44399  fourierdlem46  44400  fourierdlem47  44401  fourierdlem48  44402  fourierdlem49  44403  fourierdlem50  44404  fourierdlem63  44417  fourierdlem64  44418  fourierdlem65  44419  fourierdlem74  44428  fourierdlem75  44429  fourierdlem76  44430  fourierdlem78  44432  fourierdlem79  44433  fourierdlem89  44443  fourierdlem92  44446  fourierdlem103  44457  fourierdlem104  44458  fouriersw  44479  etransclem4  44486  etransclem23  44505  etransclem31  44513  etransclem32  44514  etransclem35  44517  etransclem41  44523  etransclem48  44530  ioorrnopnlem  44552  sge0uzfsumgt  44692  sge0seq  44694  iundjiun  44708  carageniuncllem2  44770  hoidmvlelem3  44845  iunhoiioolem  44923  vonioolem1  44928  smfmullem1  45039  smfmullem2  45040  smfmullem3  45041  bgoldbtbndlem2  46005  logbpw2m1  46660
  Copyright terms: Public domain W3C validator