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

Theorem letrd 9799
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 9734 . . 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 1872   class class class wbr 4423   RRcr 9545    <_ cle 9683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-resscn 9603  ax-pre-lttri 9620  ax-pre-lttrn 9621
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  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 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688
This theorem is referenced by:  lesub3d  10238  supmul1  10583  supmul  10586  eluzuzle  11174  iccsplit  11772  supicc  11787  fzdisj  11833  difelfzle  11911  flwordi  12053  flleceil  12086  uzsup  12096  modltm1p1mod  12148  seqf1olem1  12258  bernneq  12404  bernneq3  12406  discr1  12414  faclbnd  12481  faclbnd4lem1  12484  facubnd  12491  seqcoll  12631  sqrlem7  13312  absle  13378  releabs  13384  absrdbnd  13404  rexuzre  13415  limsupgre  13541  limsupgreOLD  13542  lo1bddrp  13588  rlimclim1  13608  rlimresb  13628  rlimrege0  13642  o1add  13676  o1sub  13678  climsqz  13703  climsqz2  13704  rlimsqzlem  13711  rlimsqz  13712  rlimsqz2  13713  rlimno1  13716  isercoll  13730  caucvgrlem  13735  caucvgrlemOLD  13736  iseraltlem3  13749  o1fsum  13872  cvgcmp  13875  cvgcmpce  13877  climcnds  13908  expcnv  13921  cvgrat  13938  mertenslem2  13940  fprodle  14049  eftlub  14162  rpnnen2  14277  bitsfzo  14408  isprm5  14650  eulerthlem2  14729  pcmpt2  14837  pcfac  14843  prmreclem3  14861  prmreclem4  14862  prmreclem5  14863  4sqlem11  14898  vdwlem1  14930  vdwlem3  14932  prdsxmetlem  21381  nrmmetd  21587  nm2dif  21636  nlmvscnlem2  21686  nmoco  21756  nmotri  21758  nghmcn  21764  icccmplem2  21839  reconnlem2  21843  elii1  21961  xrhmeo  21972  cnheiborlem  21980  bndth  21984  tchcphlem1  22207  ipcnlem2  22213  cncmet  22288  trirn  22352  minveclem2  22366  minveclem4  22372  minveclem2OLD  22378  minveclem4OLD  22384  ivthlem2  22401  ovolunlem1a  22447  ovolunlem1  22448  ovolfiniun  22452  ovoliunlem1  22453  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  ovolicc2lem5  22473  ovolicopnf  22476  nulmbl2  22488  ioombl1lem4  22512  ioorcl2  22522  uniioombllem3  22541  uniioombllem4  22542  uniioombllem5  22543  volcn  22562  vitalilem2  22565  vitali  22569  mbfi1fseqlem5  22675  mbfi1fseqlem6  22676  itg2splitlem  22704  itg2monolem1  22706  itg2monolem3  22708  itg2mono  22709  itg2cnlem1  22717  itgle  22765  bddmulibl  22794  ditgsplitlem  22813  dveflem  22929  dvlip  22943  dveq0  22950  dvfsumabs  22973  dvfsumlem1  22976  dvfsumlem2  22977  dvfsumlem3  22978  dvfsumlem4  22979  dvfsum2  22984  fta1glem2  23115  dgradd2  23220  plydiveu  23249  fta1lem  23258  aalioulem2  23287  aalioulem3  23288  aalioulem4  23289  aalioulem5  23290  aaliou3lem8  23299  aaliou3lem9  23304  ulmbdd  23351  ulmcn  23352  mtest  23357  mtestbdd  23358  abelthlem2  23385  abelthlem7  23391  pilem2  23405  pilem2OLD  23406  tanabsge  23459  cosordlem  23478  tanord  23485  logneg2  23562  abslogle  23565  dvlog2lem  23595  cxple2a  23642  abscxpbnd  23691  atans2  23855  leibpi  23866  o1cxp  23898  cxploglim2  23902  jensenlem2  23911  emcllem6  23924  harmoniclbnd  23932  harmonicubnd  23933  harmonicbnd4  23934  fsumharmonic  23935  lgamgulmlem2  23953  lgamgulmlem3  23954  lgamgulmlem5  23956  lgambdd  23960  ftalem2  23996  basellem3  24007  basellem5  24009  basellem6  24010  dvdsflsumcom  24115  fsumfldivdiaglem  24116  ppiub  24130  chtublem  24137  logfac2  24143  chpub  24146  logfacubnd  24147  logfaclbnd  24148  logfacbnd3  24149  logexprlim  24151  bcmono  24203  bpos1lem  24208  bposlem1  24210  bposlem2  24211  bposlem3  24212  bposlem4  24213  bposlem5  24214  bposlem6  24215  bposlem7  24216  bposlem9  24218  lgsdirprm  24255  lgsquadlem1  24280  2sqlem8  24298  chebbnd1lem1  24305  chebbnd1lem3  24307  chtppilimlem1  24309  chpchtlim  24315  vmadivsumb  24319  rplogsumlem1  24320  rplogsumlem2  24321  rpvmasumlem  24323  dchrisumlema  24324  dchrisumlem2  24326  dchrisumlem3  24327  dchrmusum2  24330  dchrvmasumlem2  24334  dchrvmasumlem3  24335  dchrvmasumlema  24336  dchrvmasumiflem1  24337  dchrisum0flblem1  24344  dchrisum0flblem2  24345  dchrisum0fno1  24347  dchrisum0re  24349  dchrisum0lem1b  24351  dchrisum0lem1  24352  dchrisum0lem2a  24353  dchrisum0  24356  rplogsum  24363  mudivsum  24366  mulogsumlem  24367  logdivsum  24369  mulog2sumlem1  24370  mulog2sumlem2  24371  2vmadivsumlem  24376  log2sumbnd  24380  selberglem2  24382  selbergb  24385  selberg2lem  24386  selberg2b  24388  chpdifbndlem1  24389  logdivbnd  24392  selberg3lem1  24393  selberg3lem2  24394  selberg4lem1  24396  pntrmax  24400  pntrsumo1  24401  pntrsumbnd  24402  pntrlog2bndlem1  24413  pntrlog2bndlem2  24414  pntrlog2bndlem3  24415  pntrlog2bndlem5  24417  pntrlog2bndlem6  24419  pntrlog2bnd  24420  pntpbnd1a  24421  pntpbnd1  24422  pntpbnd2  24423  pntibndlem2  24427  pntibndlem3  24428  pntlemg  24434  pntlemr  24438  pntlemj  24439  pntlemf  24441  pntlemk  24442  pntlemo  24443  pntleml  24447  abvcxp  24451  qabvle  24461  padicabv  24466  ostth2lem2  24470  ostth2lem3  24471  ostth3  24474  axlowdimlem16  24985  axcontlem8  24999  axcontlem10  25001  wwlkm1edg  25461  wwlksubclwwlk  25530  smcnlem  26331  nmoub3i  26412  ubthlem3  26512  minvecolem2  26515  minvecolem3  26516  minvecolem4  26520  minvecolem2OLD  26525  minvecolem3OLD  26526  minvecolem4OLD  26530  htthlem  26568  bcs2  26833  pjhthlem1  27042  cnlnadjlem2  27719  cnlnadjlem7  27724  nmopadjlem  27740  nmoptrii  27745  nmopcoadji  27752  leopnmid  27789  cdj1i  28084  nndiffz1  28372  pmtrto1cl  28620  psgnfzto1stlem  28621  fzto1st  28624  psgnfzto1st  28626  smatrcl  28630  submateqlem1  28641  nexple  28839  esumpcvgval  28907  oddpwdc  29195  eulerpartlems  29201  eulerpartlemgc  29203  eulerpartlemb  29209  dstfrvunirn  29315  orvclteinc  29316  ballotlemsima  29356  ballotlemfrcn0  29370  ballotlemsimaOLD  29394  ballotlemfrcn0OLD  29408  signstfveq0  29474  poimirlem6  31910  poimirlem7  31911  poimirlem13  31917  poimirlem15  31919  poimirlem29  31933  mblfinlem2  31942  mblfinlem3  31943  mblfinlem4  31944  ismblfin  31945  itg2addnc  31960  iblmulc2nc  31971  bddiblnc  31976  ftc1anclem7  31987  ftc1anclem8  31988  filbcmb  32031  geomcau  32052  prdsbnd  32089  cntotbnd  32092  bfplem2  32119  rrntotbnd  32132  iccbnd  32136  lzunuz  35579  irrapxlem3  35638  irrapxlem4  35639  irrapxlem5  35640  pellexlem2  35644  pell1qrge1  35686  monotoddzzfi  35760  jm2.17a  35780  rmygeid  35784  fzmaxdif  35801  jm2.27c  35832  jm3.1lem1  35842  expdiophlem1  35846  imo72b2lem0  36578  int-ineqtransd  36611  isprm7  36630  dvgrat  36631  monoords  37468  absnpncan2d  37474  absnpncan3d  37479  ssfiunibd  37481  leadd12dd  37492  fmul01  37598  fmul01lt1lem1  37602  fmul01lt1lem2  37603  climsuselem1  37626  climsuse  37627  dvdivbd  37735  dvbdfbdioolem2  37741  ioodvbdlimc1lem1  37743  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem1OLD  37745  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  dvnmul  37758  dvnprodlem1  37761  dvnprodlem2  37762  iblspltprt  37790  itgspltprt  37796  stoweidlem1  37801  stoweidlem3  37803  stoweidlem5  37805  stoweidlem11  37811  stoweidlem17  37817  stoweidlem20  37820  stoweidlem26  37826  stoweidlem34  37835  wallispilem4  37870  stirlinglem11  37886  stirlinglem12  37887  stirlinglem13  37888  fourierdlem12  37921  fourierdlem15  37924  fourierdlem20  37929  fourierdlem30  37939  fourierdlem39  37949  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem47  37957  fourierdlem50  37960  fourierdlem64  37974  fourierdlem65  37975  fourierdlem68  37978  fourierdlem73  37983  fourierdlem77  37987  fourierdlem79  37989  fourierdlem87  37997  elaa2lem  38037  elaa2lemOLD  38038  etransclem23  38062  sge0le  38157  sge0isum  38177  sge0xaddlem1  38183  hoicvr  38274  hsphoidmvle2  38311  hoidmv1lelem1  38317  hoidmv1lelem2  38318  hoidmv1lelem3  38319  hoidmvlelem1  38321  hoidmvlelem2  38322  hoidmvlelem4  38324  fllog2  40000
  Copyright terms: Public domain W3C validator