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

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

Proof of Theorem letrd
StepHypRef Expression
1 letrd.4 . 2  |-  ( ph  ->  A  <_  B )
2 letrd.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 letr 9127 . . 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 4176   RRcr 8949    <_ cle 9081
This theorem is referenced by:  supmul1  9933  supmul  9936  iccsplit  10989  fzdisj  11038  flwordi  11178  uzsup  11203  seqf1olem1  11321  bernneq  11464  bernneq3  11466  discr1  11474  faclbnd  11540  faclbnd4lem1  11543  facubnd  11550  seqcoll  11671  sqrlem7  12013  absle  12078  releabs  12084  absrdbnd  12104  rexuzre  12115  limsupgre  12234  lo1bddrp  12278  rlimclim1  12298  rlimresb  12318  rlimrege0  12332  o1add  12366  o1sub  12368  climsqz  12393  climsqz2  12394  rlimsqzlem  12401  rlimsqz  12402  rlimsqz2  12403  rlimno1  12406  isercoll  12420  caucvgrlem  12425  iseraltlem3  12436  o1fsum  12551  cvgcmp  12554  cvgcmpce  12556  climcnds  12590  expcnv  12602  cvgrat  12619  mertenslem2  12621  eftlub  12669  rpnnen2  12784  bitsfzo  12906  isprm5  13071  eulerthlem2  13130  pcmpt2  13221  pcfac  13227  prmreclem3  13245  prmreclem4  13246  prmreclem5  13247  4sqlem11  13282  vdwlem1  13308  vdwlem3  13310  prdsxmetlem  18355  nrmmetd  18579  nm2dif  18628  nlmvscnlem2  18678  nmoco  18728  nmotri  18730  nghmcn  18736  icccmplem2  18811  reconnlem2  18815  elii1  18917  xrhmeo  18928  cnheiborlem  18936  bndth  18940  tchcphlem1  19149  ipcnlem2  19155  cncmet  19232  minveclem2  19284  minveclem4  19290  ivthlem2  19306  ovolunlem1a  19349  ovolunlem1  19350  ovolfiniun  19354  ovoliunlem1  19355  ovolicc2lem4  19373  ovolicc2lem5  19374  ovolicopnf  19377  nulmbl2  19388  ioombl1lem4  19412  ioorcl2  19421  uniioombllem3  19434  uniioombllem4  19435  uniioombllem5  19436  volcn  19455  vitalilem2  19458  vitali  19462  mbfi1fseqlem5  19568  mbfi1fseqlem6  19569  itg2splitlem  19597  itg2monolem1  19599  itg2monolem3  19601  itg2mono  19602  itg2cnlem1  19610  itgle  19658  bddmulibl  19687  ditgsplitlem  19704  dveflem  19820  dvlip  19834  dveq0  19841  dvfsumabs  19864  dvfsumlem1  19867  dvfsumlem2  19868  dvfsumlem3  19869  dvfsumlem4  19870  dvfsum2  19875  fta1glem2  20046  dgradd2  20143  plydiveu  20172  fta1lem  20181  aalioulem2  20207  aalioulem3  20208  aalioulem4  20209  aalioulem5  20210  aaliou3lem8  20219  aaliou3lem9  20224  ulmbdd  20271  ulmcn  20272  mtest  20277  mtestbdd  20278  abelthlem2  20305  abelthlem7  20311  pilem2  20325  tanabsge  20371  cosordlem  20390  tanord  20397  logneg2  20467  abslogle  20470  dvlog2lem  20500  cxple2a  20547  abscxpbnd  20594  atans2  20728  leibpi  20739  o1cxp  20770  cxploglim2  20774  jensenlem2  20783  emcllem6  20796  harmoniclbnd  20804  harmonicubnd  20805  harmonicbnd4  20806  fsumharmonic  20807  ftalem2  20813  basellem3  20822  basellem5  20824  basellem6  20825  dvdsflsumcom  20930  fsumfldivdiaglem  20931  ppiub  20945  chtublem  20952  logfac2  20958  chpub  20961  logfacubnd  20962  logfaclbnd  20963  logfacbnd3  20964  logexprlim  20966  bcmono  21018  bpos1lem  21023  bposlem1  21025  bposlem2  21026  bposlem3  21027  bposlem4  21028  bposlem5  21029  bposlem6  21030  bposlem7  21031  bposlem9  21033  lgsdirprm  21070  lgsquadlem1  21095  2sqlem8  21113  chebbnd1lem1  21120  chebbnd1lem3  21122  chtppilimlem1  21124  chpchtlim  21130  vmadivsumb  21134  rplogsumlem1  21135  rplogsumlem2  21136  rpvmasumlem  21138  dchrisumlema  21139  dchrisumlem2  21141  dchrisumlem3  21142  dchrmusum2  21145  dchrvmasumlem2  21149  dchrvmasumlem3  21150  dchrvmasumlema  21151  dchrvmasumiflem1  21152  dchrisum0flblem1  21159  dchrisum0flblem2  21160  dchrisum0fno1  21162  dchrisum0re  21164  dchrisum0lem1b  21166  dchrisum0lem1  21167  dchrisum0lem2a  21168  dchrisum0  21171  rplogsum  21178  mudivsum  21181  mulogsumlem  21182  logdivsum  21184  mulog2sumlem1  21185  mulog2sumlem2  21186  2vmadivsumlem  21191  log2sumbnd  21195  selberglem2  21197  selbergb  21200  selberg2lem  21201  selberg2b  21203  chpdifbndlem1  21204  logdivbnd  21207  selberg3lem1  21208  selberg3lem2  21209  selberg4lem1  21211  pntrmax  21215  pntrsumo1  21216  pntrsumbnd  21217  pntrlog2bndlem1  21228  pntrlog2bndlem2  21229  pntrlog2bndlem3  21230  pntrlog2bndlem5  21232  pntrlog2bndlem6  21234  pntrlog2bnd  21235  pntpbnd1a  21236  pntpbnd1  21237  pntpbnd2  21238  pntibndlem2  21242  pntibndlem3  21243  pntlemg  21249  pntlemr  21253  pntlemj  21254  pntlemf  21256  pntlemk  21257  pntlemo  21258  pntleml  21262  abvcxp  21266  qabvle  21276  padicabv  21281  ostth2lem2  21285  ostth2lem3  21286  ostth3  21289  smcnlem  22150  nmoub3i  22231  ubthlem3  22331  minvecolem2  22334  minvecolem3  22335  minvecolem4  22339  htthlem  22377  bcs2  22641  pjhthlem1  22850  cnlnadjlem2  23528  cnlnadjlem7  23533  nmopadjlem  23549  nmoptrii  23554  nmopcoadji  23561  leopnmid  23598  cdj1i  23893  esumpcvgval  24425  dstfrvunirn  24689  orvclteinc  24690  ballotlemsima  24730  ballotlemfrcn0  24744  lgamgulmlem2  24771  lgamgulmlem3  24772  lgamgulmlem5  24774  lgambdd  24778  axlowdimlem16  25804  axcontlem8  25818  axcontlem10  25820  mblfinlem  26147  mblfinlem2  26148  mblfinlem3  26149  ismblfin  26150  itg2addnc  26162  iblmulc2nc  26173  bddiblnc  26178  filbcmb  26336  trirn  26351  geomcau  26359  prdsbnd  26396  cntotbnd  26399  bfplem2  26426  rrntotbnd  26439  iccbnd  26443  lzunuz  26720  irrapxlem3  26781  irrapxlem4  26782  irrapxlem5  26783  pellexlem2  26787  pell1qrge1  26827  monotoddzzfi  26899  jm2.17a  26919  rmygeid  26923  fzmaxdif  26940  jm2.27c  26972  jm3.1lem1  26982  expdiophlem1  26986  fmul01  27581  fmul01lt1lem1  27585  fmul01lt1lem2  27586  climsuselem1  27604  climsuse  27605  stoweidlem1  27621  stoweidlem3  27623  stoweidlem5  27625  stoweidlem11  27631  stoweidlem17  27637  stoweidlem20  27640  stoweidlem26  27646  stoweidlem34  27654  wallispilem4  27688  stirlinglem11  27704  stirlinglem12  27705  stirlinglem13  27706
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 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664  ax-resscn 9007  ax-pre-lttri 9024  ax-pre-lttrn 9025
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 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-nel 2574  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-er 6868  df-en 7073  df-dom 7074  df-sdom 7075  df-pnf 9082  df-mnf 9083  df-xr 9084  df-ltxr 9085  df-le 9086
  Copyright terms: Public domain W3C validator