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

Theorem ltletrd 10389
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 10321 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1477 . 2 (𝜑 → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 717 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2139   class class class wbr 4804  cr 10127   < clt 10266  cle 10267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-resscn 10185  ax-pre-lttri 10202  ax-pre-lttrn 10203
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272
This theorem is referenced by:  lelttrdi  10391  uzwo3  11976  rpgecl  12052  fznatpl1  12588  modabs  12897  seqf1olem1  13034  expgt1  13092  leexp2a  13110  bernneq3  13186  expnbnd  13187  expmulnbnd  13190  digit1  13192  discr1  13194  hashfun  13416  seqcoll2  13441  abssubne0  14255  icodiamlt  14373  reccn2  14526  isercolllem1  14594  isumltss  14779  fprodntriv  14871  efcllem  15007  sin01bnd  15114  cos01bnd  15115  sin01gt0  15119  eirrlem  15131  rpnnen2lem11  15152  ruclem10  15167  bitsmod  15360  bitsinv1lem  15365  smuval2  15406  prmreclem5  15826  1arith  15833  2expltfac  16001  mndodconglem  18160  sylow1lem1  18213  gzrngunit  20014  nlmvscnlem1  22691  nrginvrcnlem  22696  iccpnfhmeo  22945  cnheibor  22955  evth  22959  lebnumlem1  22961  ipcnlem1  23244  lmnn  23261  ovolicc2lem2  23486  itg2monolem1  23716  itg2monolem3  23718  dvferm1lem  23946  dvcnvre  23981  dvfsumlem3  23990  dvfsumrlim  23993  plyco0  24147  aaliou2b  24295  pilem2  24405  cosordlem  24476  logdivlti  24565  logdivle  24567  logcnlem3  24589  logcnlem4  24590  cxpcn3lem  24687  atanre  24811  atanlogaddlem  24839  atans2  24857  ressatans  24860  birthdaylem3  24879  cxp2lim  24902  cxploglim2  24904  jensenlem2  24913  harmonicubnd  24935  fsumharmonic  24937  lgamgulmlem2  24955  lgamgulmlem3  24956  lgamucov  24963  ftalem2  24999  ftalem5  25002  vma1  25091  chtrpcl  25100  ppiltx  25102  fsumfldivdiaglem  25114  chtub  25136  fsumvma2  25138  chpval2  25142  chpchtsum  25143  chpub  25144  bpos1  25207  bposlem1  25208  bposlem2  25209  bposlem6  25213  gausslemma2dlem0c  25282  lgsquadlem1  25304  chebbnd1lem1  25357  chebbnd1lem2  25358  chebbnd1lem3  25359  chebbnd1  25360  chtppilimlem1  25361  chtppilimlem2  25362  chtppilim  25363  chto1ub  25364  chebbnd2  25365  chto1lb  25366  chpchtlim  25367  chpo1ub  25368  rplogsumlem2  25373  dchrisumlema  25376  dchrisumlem3  25379  dchrmusumlema  25381  dchrvmasumlem2  25386  dchrvmasumiflem1  25389  dchrisum0lema  25402  mulog2sumlem1  25422  chpdifbndlem1  25441  chpdifbnd  25443  pntrsumo1  25453  pntpbnd1  25474  pntpbnd2  25475  pntibndlem2  25479  pntlemb  25485  pntlemh  25487  pntlemr  25490  pntlem3  25497  pnt2  25501  ostth2lem1  25506  ostth2lem3  25523  ostth2lem4  25524  axsegconlem7  26002  axsegconlem10  26005  axlowdimlem16  26036  axcontlem2  26044  axcontlem4  26046  axcontlem7  26049  clwlkclwwlklem2a2  27116  clwwlkext2edg  27186  smatrcl  30171  1smat1  30179  lmdvg  30308  dya2icoseg  30648  eulerpartlems  30731  reprlt  31006  reprinfz1  31009  breprexplemc  31019  hgt750lemd  31035  hgt750lem  31038  hgt750leme  31045  tgoldbachgtde  31047  subfacval3  31478  knoppndvlem1  32809  knoppndvlem2  32810  knoppndvlem7  32815  knoppndvlem14  32822  knoppndvlem18  32826  poimirlem7  33729  poimirlem24  33746  poimirlem29  33751  mblfinlem2  33760  itg2addnclem  33774  itg2addnclem3  33776  ftc1anclem5  33802  ftc1anclem7  33804  ftc1anc  33806  areacirclem5  33817  irrapxlem4  37891  irrapxlem5  37892  pellexlem2  37896  pell14qrgapw  37942  pellqrex  37945  pellfundgt1  37949  pellfundex  37952  ltrmxnn0  38018  jm2.24nn  38028  jm2.17c  38031  jm2.24  38032  jm2.23  38065  jm3.1lem1  38086  jm3.1lem2  38087  radcnvrat  39015  dstregt0  39992  monoords  40010  uzubioo  40297  fsumnncl  40306  mullimc  40351  mullimcf  40358  sumnnodd  40365  limcleqr  40379  addlimc  40383  0ellimcdiv  40384  limclner  40386  limsupgtlem  40512  dvdivbd  40641  ioodvbdlimc1lem1  40649  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  dvnmul  40661  iblspltprt  40692  itgspltprt  40698  stoweidlem11  40731  stoweidlem24  40744  stoweidlem25  40745  stoweidlem26  40746  stoweidlem34  40754  stoweidlem36  40756  stoweidlem42  40762  stoweidlem44  40764  stoweidlem51  40771  stoweidlem59  40779  wallispi  40790  wallispi2lem1  40791  wallispi2  40793  stirlinglem11  40804  dirkertrigeqlem1  40818  dirkeritg  40822  fourierdlem10  40837  fourierdlem11  40838  fourierdlem12  40839  fourierdlem15  40842  fourierdlem19  40846  fourierdlem20  40847  fourierdlem30  40857  fourierdlem32  40859  fourierdlem40  40867  fourierdlem41  40868  fourierdlem44  40871  fourierdlem46  40872  fourierdlem47  40873  fourierdlem48  40874  fourierdlem49  40875  fourierdlem50  40876  fourierdlem63  40889  fourierdlem64  40890  fourierdlem65  40891  fourierdlem74  40900  fourierdlem75  40901  fourierdlem76  40902  fourierdlem78  40904  fourierdlem79  40905  fourierdlem89  40915  fourierdlem92  40918  fourierdlem103  40929  fourierdlem104  40930  fouriersw  40951  etransclem4  40958  etransclem23  40977  etransclem31  40985  etransclem32  40986  etransclem35  40989  etransclem41  40995  etransclem48  41002  ioorrnopnlem  41027  sge0uzfsumgt  41164  sge0seq  41166  iundjiun  41180  carageniuncllem2  41242  hoidmvlelem3  41317  iunhoiioolem  41395  vonioolem1  41400  smfmullem1  41504  smfmullem2  41505  smfmullem3  41506  bgoldbtbndlem2  42204  logbpw2m1  42871
  Copyright terms: Public domain W3C validator