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

Theorem ltletrd 9186
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 9122 . . 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 4172   RRcr 8945    < clt 9076    <_ cle 9077
This theorem is referenced by:  uzwo3  10525  rpgecl  10593  modabs  11229  seqf1olem1  11317  expgt1  11373  leexp2a  11390  bernneq3  11462  expnbnd  11463  expmulnbnd  11466  digit1  11468  discr1  11470  hashfun  11655  seqcoll2  11668  abssubne0  12075  reccn2  12345  isercolllem1  12413  isumltss  12583  efcllem  12635  sin01bnd  12741  cos01bnd  12742  sin01gt0  12746  eirrlem  12758  rpnnen2lem11  12779  ruclem10  12793  bitsmod  12903  bitsinv1lem  12908  smuval2  12949  prmreclem5  13243  1arith  13250  2expltfac  13381  mndodconglem  15134  sylow1lem1  15187  gzrngunit  16719  nlmvscnlem1  18675  nrginvrcnlem  18679  iccpnfhmeo  18923  cnheibor  18933  evth  18937  lebnumlem1  18939  ipcnlem1  19152  lmnn  19169  ovolicc2lem2  19367  itg2monolem1  19595  itg2monolem3  19597  dvferm1lem  19821  dvcnvre  19856  dvfsumlem3  19865  dvfsumrlim  19868  plyco0  20064  aaliou2b  20211  pilem2  20321  cosordlem  20386  logdivlti  20468  logdivle  20470  logcnlem3  20488  logcnlem4  20489  cxpcn3lem  20584  atanre  20678  atanlogaddlem  20706  atans2  20724  ressatans  20727  birthdaylem3  20745  cxp2lim  20768  cxploglim2  20770  jensenlem2  20779  harmonicubnd  20801  fsumharmonic  20803  ftalem2  20809  ftalem5  20812  vma1  20902  chtrpcl  20911  ppiltx  20913  fsumfldivdiaglem  20927  chtub  20949  fsumvma2  20951  chpval2  20955  chpchtsum  20956  chpub  20957  bpos1  21020  bposlem1  21021  bposlem2  21022  bposlem6  21026  lgsquadlem1  21091  chebbnd1lem1  21116  chebbnd1lem2  21117  chebbnd1lem3  21118  chebbnd1  21119  chtppilimlem1  21120  chtppilimlem2  21121  chtppilim  21122  chto1ub  21123  chebbnd2  21124  chto1lb  21125  chpchtlim  21126  chpo1ub  21127  rplogsumlem2  21132  dchrisumlema  21135  dchrisumlem3  21138  dchrmusumlema  21140  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  dchrisum0lema  21161  mulog2sumlem1  21181  chpdifbndlem1  21200  chpdifbnd  21202  pntrsumo1  21212  pntpbnd1  21233  pntpbnd2  21234  pntibndlem2  21238  pntlemb  21244  pntlemh  21246  pntlemr  21249  pntlem3  21256  pnt2  21260  ostth2lem1  21265  ostth2lem3  21282  ostth2lem4  21283  lmdvg  24291  dya2icoseg  24580  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamucov  24775  subfacval3  24828  fznatpl1  25151  fprodntriv  25221  axsegconlem7  25766  axsegconlem10  25769  axlowdimlem16  25800  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  mblfinlem  26143  itg2addnclem  26155  itg2addnclem3  26157  areacirclem6  26186  icodiamlt  26773  irrapxlem4  26778  irrapxlem5  26779  pellexlem2  26783  pell14qrgapw  26829  pellqrex  26832  pellfundgt1  26836  pellfundex  26839  ltrmxnn0  26904  jm2.24nn  26914  jm2.17c  26917  jm2.24  26918  jm2.23  26957  jm3.1lem1  26978  jm3.1lem2  26979  stoweidlem11  27627  stoweidlem24  27640  stoweidlem25  27641  stoweidlem26  27642  stoweidlem34  27650  stoweidlem36  27652  stoweidlem42  27658  stoweidlem44  27660  stoweidlem51  27667  stoweidlem59  27675  wallispi  27686  wallispi2lem1  27687  wallispi2  27689  stirlinglem11  27700
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 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-resscn 9003  ax-pre-lttri 9020  ax-pre-lttrn 9021
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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082
  Copyright terms: Public domain W3C validator