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

Theorem ltletrd 10774
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 10706 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1367 . 2 (𝜑 → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 697 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2114   class class class wbr 5038  cr 10510   < clt 10649  cle 10650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5175  ax-nul 5182  ax-pow 5238  ax-pr 5302  ax-un 7435  ax-resscn 10568  ax-pre-lttri 10585  ax-pre-lttrn 10586
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3472  df-sbc 3749  df-csb 3857  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4811  df-br 5039  df-opab 5101  df-mpt 5119  df-id 5432  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6286  df-fun 6329  df-fn 6330  df-f 6331  df-f1 6332  df-fo 6333  df-f1o 6334  df-fv 6335  df-er 8263  df-en 8484  df-dom 8485  df-sdom 8486  df-pnf 10651  df-mnf 10652  df-xr 10653  df-ltxr 10654  df-le 10655
This theorem is referenced by:  lelttrdi  10776  uzwo3  12318  rpgecl  12392  fznatpl1  12941  modabs  13252  seqf1olem1  13390  expgt1  13448  leexp2a  13517  bernneq3  13573  expnbnd  13574  expmulnbnd  13577  digit1  13579  discr1  13581  hashfun  13779  seqcoll2  13804  abssubne0  14652  icodiamlt  14771  reccn2  14929  isercolllem1  14997  isumltss  15179  fprodntriv  15272  efcllem  15407  sin01bnd  15514  cos01bnd  15515  sin01gt0  15519  eirrlem  15533  rpnnen2lem11  15553  ruclem10  15568  bitsmod  15759  bitsinv1lem  15764  smuval2  15805  prmreclem5  16230  1arith  16237  2expltfac  16401  mndodconglem  18644  sylow1lem1  18698  gzrngunit  20583  nlmvscnlem1  23267  nrginvrcnlem  23272  iccpnfhmeo  23525  cnheibor  23535  evth  23539  lebnumlem1  23541  ipcnlem1  23824  lmnn  23842  ovolicc2lem2  24097  itg2monolem1  24329  itg2monolem3  24331  dvferm1lem  24562  dvcnvre  24597  dvfsumlem3  24606  dvfsumrlim  24609  plyco0  24764  aaliou2b  24912  pilem2  25022  cosq34lt1  25094  cosordlem  25097  logdivlti  25186  logdivle  25188  logcnlem3  25210  logcnlem4  25211  cxpcn3lem  25311  atanre  25446  atanlogaddlem  25474  atans2  25492  birthdaylem3  25514  cxp2lim  25537  cxploglim2  25539  jensenlem2  25548  harmonicubnd  25570  fsumharmonic  25572  lgamgulmlem2  25590  lgamgulmlem3  25591  lgamucov  25598  ftalem2  25634  ftalem5  25637  vma1  25726  chtrpcl  25735  ppiltx  25737  fsumfldivdiaglem  25749  chtub  25771  fsumvma2  25773  chpval2  25777  chpchtsum  25778  chpub  25779  bpos1  25842  bposlem1  25843  bposlem2  25844  bposlem6  25848  gausslemma2dlem0c  25917  lgsquadlem1  25939  chebbnd1lem1  26028  chebbnd1lem2  26029  chebbnd1lem3  26030  chebbnd1  26031  chtppilimlem1  26032  chtppilimlem2  26033  chtppilim  26034  chto1ub  26035  chebbnd2  26036  chto1lb  26037  chpchtlim  26038  chpo1ub  26039  rplogsumlem2  26044  dchrisumlema  26047  dchrisumlem3  26050  dchrmusumlema  26052  dchrvmasumlem2  26057  dchrvmasumiflem1  26060  dchrisum0lema  26073  mulog2sumlem1  26093  chpdifbndlem1  26112  chpdifbnd  26114  pntrsumo1  26124  pntpbnd1  26145  pntpbnd2  26146  pntibndlem2  26150  pntlemb  26156  pntlemh  26158  pntlemr  26161  pntlem3  26168  pnt2  26172  ostth2lem1  26177  ostth2lem3  26194  ostth2lem4  26195  axsegconlem7  26692  axsegconlem10  26695  axlowdimlem16  26726  axcontlem2  26734  axcontlem4  26736  axcontlem7  26739  clwlkclwwlklem2a2  27753  clwwlkext2edg  27816  smatrcl  31068  1smat1  31076  lmdvg  31200  dya2icoseg  31539  eulerpartlems  31622  reprlt  31894  reprinfz1  31897  breprexplemc  31907  hgt750lemd  31923  hgt750lem  31926  hgt750leme  31933  tgoldbachgtde  31935  subfacval3  32440  knoppndvlem1  33855  knoppndvlem2  33856  knoppndvlem7  33861  knoppndvlem14  33868  knoppndvlem18  33872  poimirlem7  34936  poimirlem24  34953  poimirlem29  34958  mblfinlem2  34967  itg2addnclem  34980  itg2addnclem3  34982  ftc1anclem5  35006  ftc1anclem7  35008  ftc1anc  35010  areacirclem5  35021  lcmineqlem23  39199  3cubeslem1  39414  irrapxlem4  39555  irrapxlem5  39556  pellexlem2  39560  pell14qrgapw  39606  pellqrex  39609  pellfundgt1  39613  pellfundex  39616  ltrmxnn0  39679  jm2.24nn  39689  jm2.17c  39692  jm2.24  39693  jm2.23  39726  jm3.1lem1  39747  jm3.1lem2  39748  radcnvrat  40797  dstregt0  41697  monoords  41714  uzubioo  41991  fsumnncl  42000  mullimc  42045  mullimcf  42052  sumnnodd  42059  limcleqr  42073  addlimc  42077  0ellimcdiv  42078  limclner  42080  limsupgtlem  42206  dvdivbd  42352  ioodvbdlimc1lem1  42360  ioodvbdlimc1lem2  42361  ioodvbdlimc2lem  42363  dvnmul  42372  iblspltprt  42402  itgspltprt  42408  stoweidlem11  42440  stoweidlem24  42453  stoweidlem25  42454  stoweidlem26  42455  stoweidlem34  42463  stoweidlem36  42465  stoweidlem42  42471  stoweidlem44  42473  stoweidlem51  42480  stoweidlem59  42488  wallispi  42499  wallispi2lem1  42500  wallispi2  42502  stirlinglem11  42513  dirkertrigeqlem1  42527  dirkeritg  42531  fourierdlem10  42546  fourierdlem11  42547  fourierdlem12  42548  fourierdlem15  42551  fourierdlem19  42555  fourierdlem20  42556  fourierdlem30  42566  fourierdlem32  42568  fourierdlem40  42576  fourierdlem41  42577  fourierdlem44  42580  fourierdlem46  42581  fourierdlem47  42582  fourierdlem48  42583  fourierdlem49  42584  fourierdlem50  42585  fourierdlem63  42598  fourierdlem64  42599  fourierdlem65  42600  fourierdlem74  42609  fourierdlem75  42610  fourierdlem76  42611  fourierdlem78  42613  fourierdlem79  42614  fourierdlem89  42624  fourierdlem92  42627  fourierdlem103  42638  fourierdlem104  42639  fouriersw  42660  etransclem4  42667  etransclem23  42686  etransclem31  42694  etransclem32  42695  etransclem35  42698  etransclem41  42704  etransclem48  42711  ioorrnopnlem  42733  sge0uzfsumgt  42870  sge0seq  42872  iundjiun  42886  carageniuncllem2  42948  hoidmvlelem3  43023  iunhoiioolem  43101  vonioolem1  43106  smfmullem1  43210  smfmullem2  43211  smfmullem3  43212  bgoldbtbndlem2  44112  logbpw2m1  44768
  Copyright terms: Public domain W3C validator