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

Theorem ltletrd 9194
Description: Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.)
Hypotheses
Ref Expression
ltd.1  |-  ( ph  ->  A  e.  RR )
ltd.2  |-  ( ph  ->  B  e.  RR )
letrd.3  |-  ( ph  ->  C  e.  RR )
ltletrd.4  |-  ( ph  ->  A  <  B )
ltletrd.5  |-  ( ph  ->  B  <_  C )
Assertion
Ref Expression
ltletrd  |-  ( ph  ->  A  <  C )

Proof of Theorem ltletrd
StepHypRef Expression
1 ltletrd.4 . 2  |-  ( ph  ->  A  <  B )
2 ltletrd.5 . 2  |-  ( ph  ->  B  <_  C )
3 ltd.1 . . 3  |-  ( ph  ->  A  e.  RR )
4 ltd.2 . . 3  |-  ( ph  ->  B  e.  RR )
5 letrd.3 . . 3  |-  ( ph  ->  C  e.  RR )
6 ltletr 9130 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <  B  /\  B  <_  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1184 . 2  |-  ( ph  ->  ( ( A  < 
B  /\  B  <_  C )  ->  A  <  C ) )
81, 2, 7mp2and 661 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   class class class wbr 4180   RRcr 8953    < clt 9084    <_ cle 9085
This theorem is referenced by:  uzwo3  10533  rpgecl  10601  modabs  11237  seqf1olem1  11325  expgt1  11381  leexp2a  11398  bernneq3  11470  expnbnd  11471  expmulnbnd  11474  digit1  11476  discr1  11478  hashfun  11663  seqcoll2  11676  abssubne0  12083  reccn2  12353  isercolllem1  12421  isumltss  12591  efcllem  12643  sin01bnd  12749  cos01bnd  12750  sin01gt0  12754  eirrlem  12766  rpnnen2lem11  12787  ruclem10  12801  bitsmod  12911  bitsinv1lem  12916  smuval2  12957  prmreclem5  13251  1arith  13258  2expltfac  13389  mndodconglem  15142  sylow1lem1  15195  gzrngunit  16727  nlmvscnlem1  18683  nrginvrcnlem  18687  iccpnfhmeo  18931  cnheibor  18941  evth  18945  lebnumlem1  18947  ipcnlem1  19160  lmnn  19177  ovolicc2lem2  19375  itg2monolem1  19603  itg2monolem3  19605  dvferm1lem  19829  dvcnvre  19864  dvfsumlem3  19873  dvfsumrlim  19876  plyco0  20072  aaliou2b  20219  pilem2  20329  cosordlem  20394  logdivlti  20476  logdivle  20478  logcnlem3  20496  logcnlem4  20497  cxpcn3lem  20592  atanre  20686  atanlogaddlem  20714  atans2  20732  ressatans  20735  birthdaylem3  20753  cxp2lim  20776  cxploglim2  20778  jensenlem2  20787  harmonicubnd  20809  fsumharmonic  20811  ftalem2  20817  ftalem5  20820  vma1  20910  chtrpcl  20919  ppiltx  20921  fsumfldivdiaglem  20935  chtub  20957  fsumvma2  20959  chpval2  20963  chpchtsum  20964  chpub  20965  bpos1  21028  bposlem1  21029  bposlem2  21030  bposlem6  21034  lgsquadlem1  21099  chebbnd1lem1  21124  chebbnd1lem2  21125  chebbnd1lem3  21126  chebbnd1  21127  chtppilimlem1  21128  chtppilimlem2  21129  chtppilim  21130  chto1ub  21131  chebbnd2  21132  chto1lb  21133  chpchtlim  21134  chpo1ub  21135  rplogsumlem2  21140  dchrisumlema  21143  dchrisumlem3  21146  dchrmusumlema  21148  dchrvmasumlem2  21153  dchrvmasumiflem1  21156  dchrisum0lema  21169  mulog2sumlem1  21189  chpdifbndlem1  21208  chpdifbnd  21210  pntrsumo1  21220  pntpbnd1  21241  pntpbnd2  21242  pntibndlem2  21246  pntlemb  21252  pntlemh  21254  pntlemr  21257  pntlem3  21264  pnt2  21268  ostth2lem1  21273  ostth2lem3  21290  ostth2lem4  21291  lmdvg  24299  dya2icoseg  24588  lgamgulmlem2  24775  lgamgulmlem3  24776  lgamucov  24783  subfacval3  24836  fznatpl1  25159  fprodntriv  25229  axsegconlem7  25774  axsegconlem10  25777  axlowdimlem16  25808  axcontlem2  25816  axcontlem4  25818  axcontlem7  25821  mblfinlem  26151  itg2addnclem  26163  itg2addnclem3  26165  areacirclem6  26194  icodiamlt  26781  irrapxlem4  26786  irrapxlem5  26787  pellexlem2  26791  pell14qrgapw  26837  pellqrex  26840  pellfundgt1  26844  pellfundex  26847  ltrmxnn0  26912  jm2.24nn  26922  jm2.17c  26925  jm2.24  26926  jm2.23  26965  jm3.1lem1  26986  jm3.1lem2  26987  stoweidlem11  27635  stoweidlem24  27648  stoweidlem25  27649  stoweidlem26  27650  stoweidlem34  27658  stoweidlem36  27660  stoweidlem42  27666  stoweidlem44  27668  stoweidlem51  27675  stoweidlem59  27683  wallispi  27694  wallispi2lem1  27695  wallispi2  27697  stirlinglem11  27708
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-resscn 9011  ax-pre-lttri 9028  ax-pre-lttrn 9029
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-er 6872  df-en 7077  df-dom 7078  df-sdom 7079  df-pnf 9086  df-mnf 9087  df-xr 9088  df-ltxr 9089  df-le 9090
  Copyright terms: Public domain W3C validator