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

Theorem letrd 9791
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 9726 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <_  C )  ->  A  <_  C
) )
73, 4, 5, 6syl3anc 1264 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <_  C
)  ->  A  <_  C ) )
81, 2, 7mp2and 683 1  |-  ( ph  ->  A  <_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1870   class class class wbr 4426   RRcr 9537    <_ cle 9675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-resscn 9595  ax-pre-lttri 9612  ax-pre-lttrn 9613
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680
This theorem is referenced by:  lesub3d  10230  supmul1  10576  supmul  10579  eluzuzle  11167  iccsplit  11763  supicc  11778  fzdisj  11824  difelfzle  11902  flwordi  12044  flleceil  12077  uzsup  12087  modltm1p1mod  12139  seqf1olem1  12249  bernneq  12395  bernneq3  12397  discr1  12405  faclbnd  12472  faclbnd4lem1  12475  facubnd  12482  seqcoll  12621  sqrlem7  13291  absle  13357  releabs  13363  absrdbnd  13383  rexuzre  13394  limsupgre  13520  limsupgreOLD  13521  lo1bddrp  13567  rlimclim1  13587  rlimresb  13607  rlimrege0  13621  o1add  13655  o1sub  13657  climsqz  13682  climsqz2  13683  rlimsqzlem  13690  rlimsqz  13691  rlimsqz2  13692  rlimno1  13695  isercoll  13709  caucvgrlem  13714  caucvgrlemOLD  13715  iseraltlem3  13728  o1fsum  13851  cvgcmp  13854  cvgcmpce  13856  climcnds  13887  expcnv  13900  cvgrat  13917  mertenslem2  13919  fprodle  14028  eftlub  14141  rpnnen2  14256  bitsfzo  14383  isprm5  14613  eulerthlem2  14690  pcmpt2  14792  pcfac  14798  prmreclem3  14816  prmreclem4  14817  prmreclem5  14818  4sqlem11  14853  vdwlem1  14885  vdwlem3  14887  prdsxmetlem  21305  nrmmetd  21511  nm2dif  21560  nlmvscnlem2  21610  nmoco  21660  nmotri  21662  nghmcn  21668  icccmplem2  21743  reconnlem2  21747  elii1  21850  xrhmeo  21861  cnheiborlem  21869  bndth  21873  tchcphlem1  22093  ipcnlem2  22099  cncmet  22174  trirn  22238  minveclem2  22252  minveclem4  22258  ivthlem2  22275  ovolunlem1a  22318  ovolunlem1  22319  ovolfiniun  22323  ovoliunlem1  22324  ovolicc2lem4  22342  ovolicc2lem5  22343  ovolicopnf  22346  nulmbl2  22358  ioombl1lem4  22382  ioorcl2  22392  uniioombllem3  22411  uniioombllem4  22412  uniioombllem5  22413  volcn  22432  vitalilem2  22435  vitali  22439  mbfi1fseqlem5  22545  mbfi1fseqlem6  22546  itg2splitlem  22574  itg2monolem1  22576  itg2monolem3  22578  itg2mono  22579  itg2cnlem1  22587  itgle  22635  bddmulibl  22664  ditgsplitlem  22683  dveflem  22799  dvlip  22813  dveq0  22820  dvfsumabs  22843  dvfsumlem1  22846  dvfsumlem2  22847  dvfsumlem3  22848  dvfsumlem4  22849  dvfsum2  22854  fta1glem2  22983  dgradd2  23081  plydiveu  23110  fta1lem  23119  aalioulem2  23145  aalioulem3  23146  aalioulem4  23147  aalioulem5  23148  aaliou3lem8  23157  aaliou3lem9  23162  ulmbdd  23209  ulmcn  23210  mtest  23215  mtestbdd  23216  abelthlem2  23243  abelthlem7  23249  pilem2  23263  pilem2OLD  23264  tanabsge  23317  cosordlem  23336  tanord  23343  logneg2  23420  abslogle  23423  dvlog2lem  23453  cxple2a  23500  abscxpbnd  23549  atans2  23713  leibpi  23724  o1cxp  23756  cxploglim2  23760  jensenlem2  23769  emcllem6  23782  harmoniclbnd  23790  harmonicubnd  23791  harmonicbnd4  23792  fsumharmonic  23793  lgamgulmlem2  23811  lgamgulmlem3  23812  lgamgulmlem5  23814  lgambdd  23818  ftalem2  23854  basellem3  23863  basellem5  23865  basellem6  23866  dvdsflsumcom  23971  fsumfldivdiaglem  23972  ppiub  23986  chtublem  23993  logfac2  23999  chpub  24002  logfacubnd  24003  logfaclbnd  24004  logfacbnd3  24005  logexprlim  24007  bcmono  24059  bpos1lem  24064  bposlem1  24066  bposlem2  24067  bposlem3  24068  bposlem4  24069  bposlem5  24070  bposlem6  24071  bposlem7  24072  bposlem9  24074  lgsdirprm  24111  lgsquadlem1  24136  2sqlem8  24154  chebbnd1lem1  24161  chebbnd1lem3  24163  chtppilimlem1  24165  chpchtlim  24171  vmadivsumb  24175  rplogsumlem1  24176  rplogsumlem2  24177  rpvmasumlem  24179  dchrisumlema  24180  dchrisumlem2  24182  dchrisumlem3  24183  dchrmusum2  24186  dchrvmasumlem2  24190  dchrvmasumlem3  24191  dchrvmasumlema  24192  dchrvmasumiflem1  24193  dchrisum0flblem1  24200  dchrisum0flblem2  24201  dchrisum0fno1  24203  dchrisum0re  24205  dchrisum0lem1b  24207  dchrisum0lem1  24208  dchrisum0lem2a  24209  dchrisum0  24212  rplogsum  24219  mudivsum  24222  mulogsumlem  24223  logdivsum  24225  mulog2sumlem1  24226  mulog2sumlem2  24227  2vmadivsumlem  24232  log2sumbnd  24236  selberglem2  24238  selbergb  24241  selberg2lem  24242  selberg2b  24244  chpdifbndlem1  24245  logdivbnd  24248  selberg3lem1  24249  selberg3lem2  24250  selberg4lem1  24252  pntrmax  24256  pntrsumo1  24257  pntrsumbnd  24258  pntrlog2bndlem1  24269  pntrlog2bndlem2  24270  pntrlog2bndlem3  24271  pntrlog2bndlem5  24273  pntrlog2bndlem6  24275  pntrlog2bnd  24276  pntpbnd1a  24277  pntpbnd1  24278  pntpbnd2  24279  pntibndlem2  24283  pntibndlem3  24284  pntlemg  24290  pntlemr  24294  pntlemj  24295  pntlemf  24297  pntlemk  24298  pntlemo  24299  pntleml  24303  abvcxp  24307  qabvle  24317  padicabv  24322  ostth2lem2  24326  ostth2lem3  24327  ostth3  24330  axlowdimlem16  24824  axcontlem8  24838  axcontlem10  24840  wwlkm1edg  25299  wwlksubclwwlk  25368  smcnlem  26169  nmoub3i  26250  ubthlem3  26350  minvecolem2  26353  minvecolem3  26354  minvecolem4  26358  htthlem  26396  bcs2  26661  pjhthlem1  26870  cnlnadjlem2  27547  cnlnadjlem7  27552  nmopadjlem  27568  nmoptrii  27573  nmopcoadji  27580  leopnmid  27617  cdj1i  27912  nndiffz1  28193  pmtrto1cl  28442  psgnfzto1stlem  28443  fzto1st  28446  psgnfzto1st  28448  smatrcl  28452  submateqlem1  28463  nexple  28661  esumpcvgval  28729  oddpwdc  29004  eulerpartlems  29010  eulerpartlemgc  29012  eulerpartlemb  29018  dstfrvunirn  29124  orvclteinc  29125  ballotlemsima  29165  ballotlemfrcn0  29179  signstfveq0  29245  poimirlem6  31640  poimirlem7  31641  poimirlem13  31647  poimirlem15  31649  poimirlem29  31663  mblfinlem2  31672  mblfinlem3  31673  mblfinlem4  31674  ismblfin  31675  itg2addnc  31690  iblmulc2nc  31701  bddiblnc  31706  ftc1anclem7  31717  ftc1anclem8  31718  filbcmb  31761  geomcau  31782  prdsbnd  31819  cntotbnd  31822  bfplem2  31849  rrntotbnd  31862  iccbnd  31866  lzunuz  35309  irrapxlem3  35368  irrapxlem4  35369  irrapxlem5  35370  pellexlem2  35374  pell1qrge1  35414  monotoddzzfi  35486  jm2.17a  35506  rmygeid  35510  fzmaxdif  35527  jm2.27c  35558  jm3.1lem1  35568  expdiophlem1  35572  imo72b2lem0  36235  int-ineqtransd  36268  isprm7  36287  dvgrat  36288  monoords  37113  absnpncan2d  37119  absnpncan3d  37124  ssfiunibd  37126  leadd12dd  37137  fmul01  37220  fmul01lt1lem1  37224  fmul01lt1lem2  37225  climsuselem1  37248  climsuse  37249  dvdivbd  37357  dvbdfbdioolem2  37363  ioodvbdlimc1lem1  37365  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  dvnmul  37377  dvnprodlem1  37380  dvnprodlem2  37381  iblspltprt  37409  itgspltprt  37415  stoweidlem1  37420  stoweidlem3  37422  stoweidlem5  37424  stoweidlem11  37430  stoweidlem17  37436  stoweidlem20  37439  stoweidlem26  37445  stoweidlem34  37454  wallispilem4  37489  stirlinglem11  37505  stirlinglem12  37506  stirlinglem13  37507  fourierdlem12  37540  fourierdlem15  37543  fourierdlem20  37548  fourierdlem30  37558  fourierdlem39  37567  fourierdlem42  37570  fourierdlem47  37575  fourierdlem50  37578  fourierdlem64  37592  fourierdlem65  37593  fourierdlem68  37596  fourierdlem73  37601  fourierdlem77  37605  fourierdlem79  37607  fourierdlem87  37615  elaa2lem  37655  etransclem23  37679  sge0le  37773  fllog2  39130
  Copyright terms: Public domain W3C validator