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

Theorem letrd 9063
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 9004 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <_  C )  ->  A  <_  C
) )
73, 4, 5, 6syl3anc 1182 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <_  C
)  ->  A  <_  C ) )
81, 2, 7mp2and 660 1  |-  ( ph  ->  A  <_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1710   class class class wbr 4104   RRcr 8826    <_ cle 8958
This theorem is referenced by:  supmul1  9809  supmul  9812  iccsplit  10860  fzdisj  10909  flwordi  11034  uzsup  11059  seqf1olem1  11177  bernneq  11320  bernneq3  11322  discr1  11330  faclbnd  11396  faclbnd4lem1  11399  facubnd  11406  seqcoll  11497  sqrlem7  11830  absle  11895  releabs  11901  absrdbnd  11921  rexuzre  11932  limsupgre  12051  lo1bddrp  12095  rlimclim1  12115  rlimresb  12135  rlimrege0  12149  o1add  12183  o1sub  12185  climsqz  12210  climsqz2  12211  rlimsqzlem  12218  rlimsqz  12219  rlimsqz2  12220  rlimno1  12223  isercoll  12237  caucvgrlem  12242  iseraltlem3  12253  o1fsum  12368  cvgcmp  12371  cvgcmpce  12373  climcnds  12407  expcnv  12419  cvgrat  12436  mertenslem2  12438  eftlub  12486  rpnnen2  12601  bitsfzo  12723  isprm5  12888  eulerthlem2  12947  pcmpt2  13038  pcfac  13044  prmreclem3  13062  prmreclem4  13063  prmreclem5  13064  4sqlem11  13099  vdwlem1  13125  vdwlem3  13127  prdsxmetlem  18034  nrmmetd  18199  nm2dif  18248  nlmvscnlem2  18298  nmoco  18348  nmotri  18350  nghmcn  18356  icccmplem2  18431  reconnlem2  18435  elii1  18537  xrhmeo  18548  cnheiborlem  18556  bndth  18560  tchcphlem1  18769  ipcnlem2  18775  cncmet  18848  minveclem2  18894  minveclem4  18900  ivthlem2  18916  ovolunlem1a  18959  ovolunlem1  18960  ovolfiniun  18964  ovoliunlem1  18965  ovolicc2lem4  18983  ovolicc2lem5  18984  ovolicopnf  18987  nulmbl2  18998  ioombl1lem4  19022  ioorcl2  19031  uniioombllem3  19044  uniioombllem4  19045  uniioombllem5  19046  volcn  19065  vitalilem2  19068  vitali  19072  mbfi1fseqlem5  19178  mbfi1fseqlem6  19179  itg2splitlem  19207  itg2monolem1  19209  itg2monolem3  19211  itg2mono  19212  itg2cnlem1  19220  itgle  19268  bddmulibl  19297  ditgsplitlem  19314  dveflem  19430  dvlip  19444  dveq0  19451  dvfsumabs  19474  dvfsumlem1  19477  dvfsumlem2  19478  dvfsumlem3  19479  dvfsumlem4  19480  dvfsum2  19485  fta1glem2  19656  dgradd2  19753  plydiveu  19782  fta1lem  19791  aalioulem2  19817  aalioulem3  19818  aalioulem4  19819  aalioulem5  19820  aaliou3lem8  19829  aaliou3lem9  19834  ulmbdd  19881  ulmcn  19882  mtest  19887  mtestbdd  19888  abelthlem2  19915  abelthlem7  19921  pilem2  19935  tanabsge  19981  cosordlem  20000  tanord  20007  logneg2  20077  abslogle  20080  dvlog2lem  20110  cxple2a  20157  abscxpbnd  20204  atans2  20338  leibpi  20349  o1cxp  20380  cxploglim2  20384  jensenlem2  20393  emcllem6  20406  harmoniclbnd  20414  harmonicubnd  20415  harmonicbnd4  20416  fsumharmonic  20417  ftalem2  20423  basellem3  20432  basellem5  20434  basellem6  20435  dvdsflsumcom  20540  fsumfldivdiaglem  20541  ppiub  20555  chtublem  20562  logfac2  20568  chpub  20571  logfacubnd  20572  logfaclbnd  20573  logfacbnd3  20574  logexprlim  20576  bcmono  20628  bpos1lem  20633  bposlem1  20635  bposlem2  20636  bposlem3  20637  bposlem4  20638  bposlem5  20639  bposlem6  20640  bposlem7  20641  bposlem9  20643  lgsdirprm  20680  lgsquadlem1  20705  2sqlem8  20723  chebbnd1lem1  20730  chebbnd1lem3  20732  chtppilimlem1  20734  chpchtlim  20740  vmadivsumb  20744  rplogsumlem1  20745  rplogsumlem2  20746  rpvmasumlem  20748  dchrisumlema  20749  dchrisumlem2  20751  dchrisumlem3  20752  dchrmusum2  20755  dchrvmasumlem2  20759  dchrvmasumlem3  20760  dchrvmasumlema  20761  dchrvmasumiflem1  20762  dchrisum0flblem1  20769  dchrisum0flblem2  20770  dchrisum0fno1  20772  dchrisum0re  20774  dchrisum0lem1b  20776  dchrisum0lem1  20777  dchrisum0lem2a  20778  dchrisum0  20781  rplogsum  20788  mudivsum  20791  mulogsumlem  20792  logdivsum  20794  mulog2sumlem1  20795  mulog2sumlem2  20796  2vmadivsumlem  20801  log2sumbnd  20805  selberglem2  20807  selbergb  20810  selberg2lem  20811  selberg2b  20813  chpdifbndlem1  20814  logdivbnd  20817  selberg3lem1  20818  selberg3lem2  20819  selberg4lem1  20821  pntrmax  20825  pntrsumo1  20826  pntrsumbnd  20827  pntrlog2bndlem1  20838  pntrlog2bndlem2  20839  pntrlog2bndlem3  20840  pntrlog2bndlem5  20842  pntrlog2bndlem6  20844  pntrlog2bnd  20845  pntpbnd1a  20846  pntpbnd1  20847  pntpbnd2  20848  pntibndlem2  20852  pntibndlem3  20853  pntlemg  20859  pntlemr  20863  pntlemj  20864  pntlemf  20866  pntlemk  20867  pntlemo  20868  pntleml  20872  abvcxp  20876  qabvle  20886  padicabv  20891  ostth2lem2  20895  ostth2lem3  20896  ostth3  20899  smcnlem  21384  nmoub3i  21465  ubthlem3  21565  minvecolem2  21568  minvecolem3  21569  minvecolem4  21573  htthlem  21611  bcs2  21875  pjhthlem1  22084  cnlnadjlem2  22762  cnlnadjlem7  22767  nmopadjlem  22783  nmoptrii  22788  nmopcoadji  22795  leopnmid  22832  cdj1i  23127  esumpcvgval  23734  dstfrvunirn  23981  ballotlemsdom  24018  ballotlemsima  24022  ballotlemfrcn0  24036  lgamgulmlem2  24063  lgamgulmlem3  24064  lgamgulmlem5  24066  lgambdd  24070  axlowdimlem16  25144  axcontlem8  25158  axcontlem10  25160  itg2addnc  25494  iblmulc2nc  25505  bddiblnc  25510  filbcmb  25756  trirn  25787  geomcau  25799  prdsbnd  25840  cntotbnd  25843  bfplem2  25870  rrntotbnd  25883  iccbnd  25887  lzunuz  26170  irrapxlem3  26232  irrapxlem4  26233  irrapxlem5  26234  pellexlem2  26238  pell1qrge1  26278  monotoddzzfi  26350  jm2.17a  26370  rmygeid  26374  fzmaxdif  26391  jm2.27c  26423  jm3.1lem1  26433  expdiophlem1  26437  climsuselem1  27056  climsuse  27057  stirlinglem11  27156  stirlinglem12  27157  stirlinglem13  27158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594  ax-resscn 8884  ax-pre-lttri 8901  ax-pre-lttrn 8902
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-er 6747  df-en 6952  df-dom 6953  df-sdom 6954  df-pnf 8959  df-mnf 8960  df-xr 8961  df-ltxr 8962  df-le 8963
  Copyright terms: Public domain W3C validator