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

Theorem ltletrd 9235
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 9171 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <  B  /\  B  <_  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1185 . 2  |-  ( ph  ->  ( ( A  < 
B  /\  B  <_  C )  ->  A  <  C ) )
81, 2, 7mp2and 662 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726   class class class wbr 4215   RRcr 8994    < clt 9125    <_ cle 9126
This theorem is referenced by:  uzwo3  10574  rpgecl  10642  modabs  11279  seqf1olem1  11367  expgt1  11423  leexp2a  11440  bernneq3  11512  expnbnd  11513  expmulnbnd  11516  digit1  11518  discr1  11520  hashfun  11705  seqcoll2  11718  abssubne0  12125  reccn2  12395  isercolllem1  12463  isumltss  12633  efcllem  12685  sin01bnd  12791  cos01bnd  12792  sin01gt0  12796  eirrlem  12808  rpnnen2lem11  12829  ruclem10  12843  bitsmod  12953  bitsinv1lem  12958  smuval2  12999  prmreclem5  13293  1arith  13300  2expltfac  13431  mndodconglem  15184  sylow1lem1  15237  gzrngunit  16769  nlmvscnlem1  18727  nrginvrcnlem  18731  iccpnfhmeo  18975  cnheibor  18985  evth  18989  lebnumlem1  18991  ipcnlem1  19204  lmnn  19221  ovolicc2lem2  19419  itg2monolem1  19645  itg2monolem3  19647  dvferm1lem  19873  dvcnvre  19908  dvfsumlem3  19917  dvfsumrlim  19920  plyco0  20116  aaliou2b  20263  pilem2  20373  cosordlem  20438  logdivlti  20520  logdivle  20522  logcnlem3  20540  logcnlem4  20541  cxpcn3lem  20636  atanre  20730  atanlogaddlem  20758  atans2  20776  ressatans  20779  birthdaylem3  20797  cxp2lim  20820  cxploglim2  20822  jensenlem2  20831  harmonicubnd  20853  fsumharmonic  20855  ftalem2  20861  ftalem5  20864  vma1  20954  chtrpcl  20963  ppiltx  20965  fsumfldivdiaglem  20979  chtub  21001  fsumvma2  21003  chpval2  21007  chpchtsum  21008  chpub  21009  bpos1  21072  bposlem1  21073  bposlem2  21074  bposlem6  21078  lgsquadlem1  21143  chebbnd1lem1  21168  chebbnd1lem2  21169  chebbnd1lem3  21170  chebbnd1  21171  chtppilimlem1  21172  chtppilimlem2  21173  chtppilim  21174  chto1ub  21175  chebbnd2  21176  chto1lb  21177  chpchtlim  21178  chpo1ub  21179  rplogsumlem2  21184  dchrisumlema  21187  dchrisumlem3  21190  dchrmusumlema  21192  dchrvmasumlem2  21197  dchrvmasumiflem1  21200  dchrisum0lema  21213  mulog2sumlem1  21233  chpdifbndlem1  21252  chpdifbnd  21254  pntrsumo1  21264  pntpbnd1  21285  pntpbnd2  21286  pntibndlem2  21290  pntlemb  21296  pntlemh  21298  pntlemr  21301  pntlem3  21308  pnt2  21312  ostth2lem1  21317  ostth2lem3  21334  ostth2lem4  21335  lmdvg  24343  dya2icoseg  24632  lgamgulmlem2  24819  lgamgulmlem3  24820  lgamucov  24827  subfacval3  24880  fznatpl1  25203  fprodntriv  25273  axsegconlem7  25867  axsegconlem10  25870  axlowdimlem16  25901  axcontlem2  25909  axcontlem4  25911  axcontlem7  25914  mblfinlem2  26256  itg2addnclem  26270  itg2addnclem3  26272  ftc1anclem5  26298  ftc1anclem7  26300  ftc1anc  26302  areacirclem5  26310  icodiamlt  26897  irrapxlem4  26902  irrapxlem5  26903  pellexlem2  26907  pell14qrgapw  26953  pellqrex  26956  pellfundgt1  26960  pellfundex  26963  ltrmxnn0  27028  jm2.24nn  27038  jm2.17c  27041  jm2.24  27042  jm2.23  27081  jm3.1lem1  27102  jm3.1lem2  27103  stoweidlem11  27750  stoweidlem24  27763  stoweidlem25  27764  stoweidlem26  27765  stoweidlem34  27773  stoweidlem36  27775  stoweidlem42  27781  stoweidlem44  27783  stoweidlem51  27790  stoweidlem59  27798  wallispi  27809  wallispi2lem1  27810  wallispi2  27812  stirlinglem11  27823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-resscn 9052  ax-pre-lttri 9069  ax-pre-lttrn 9070
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-er 6908  df-en 7113  df-dom 7114  df-sdom 7115  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131
  Copyright terms: Public domain W3C validator