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

Theorem letrd 9742
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 9681 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <_  C )  ->  A  <_  C
) )
73, 4, 5, 6syl3anc 1229 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <_  C
)  ->  A  <_  C ) )
81, 2, 7mp2and 679 1  |-  ( ph  ->  A  <_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804   class class class wbr 4437   RRcr 9494    <_ cle 9632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-pre-lttri 9569  ax-pre-lttrn 9570
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637
This theorem is referenced by:  supmul1  10515  supmul  10518  eluzuzle  11100  iccsplit  11664  supicc  11679  fzdisj  11723  difelfzle  11799  flwordi  11930  flleceil  11962  uzsup  11972  modltm1p1mod  12021  seqf1olem1  12128  bernneq  12274  bernneq3  12276  discr1  12284  faclbnd  12350  faclbnd4lem1  12353  facubnd  12360  seqcoll  12494  swrdn0  12637  sqrlem7  13064  absle  13130  releabs  13136  absrdbnd  13156  rexuzre  13167  limsupgre  13286  lo1bddrp  13330  rlimclim1  13350  rlimresb  13370  rlimrege0  13384  o1add  13418  o1sub  13420  climsqz  13445  climsqz2  13446  rlimsqzlem  13453  rlimsqz  13454  rlimsqz2  13455  rlimno1  13458  isercoll  13472  caucvgrlem  13477  iseraltlem3  13488  o1fsum  13609  cvgcmp  13612  cvgcmpce  13614  climcnds  13645  expcnv  13657  cvgrat  13674  mertenslem2  13676  eftlub  13826  rpnnen2  13941  bitsfzo  14067  isprm5  14235  eulerthlem2  14294  pcmpt2  14394  pcfac  14400  prmreclem3  14418  prmreclem4  14419  prmreclem5  14420  4sqlem11  14455  vdwlem1  14481  vdwlem3  14483  prdsxmetlem  20849  nrmmetd  21073  nm2dif  21122  nlmvscnlem2  21172  nmoco  21222  nmotri  21224  nghmcn  21230  icccmplem2  21306  reconnlem2  21310  elii1  21413  xrhmeo  21424  cnheiborlem  21432  bndth  21436  tchcphlem1  21656  ipcnlem2  21662  cncmet  21739  trirn  21805  minveclem2  21819  minveclem4  21825  ivthlem2  21842  ovolunlem1a  21885  ovolunlem1  21886  ovolfiniun  21890  ovoliunlem1  21891  ovolicc2lem4  21909  ovolicc2lem5  21910  ovolicopnf  21913  nulmbl2  21925  ioombl1lem4  21949  ioorcl2  21959  uniioombllem3  21972  uniioombllem4  21973  uniioombllem5  21974  volcn  21993  vitalilem2  21996  vitali  22000  mbfi1fseqlem5  22104  mbfi1fseqlem6  22105  itg2splitlem  22133  itg2monolem1  22135  itg2monolem3  22137  itg2mono  22138  itg2cnlem1  22146  itgle  22194  bddmulibl  22223  ditgsplitlem  22242  dveflem  22358  dvlip  22372  dveq0  22379  dvfsumabs  22402  dvfsumlem1  22405  dvfsumlem2  22406  dvfsumlem3  22407  dvfsumlem4  22408  dvfsum2  22413  fta1glem2  22545  dgradd2  22643  plydiveu  22672  fta1lem  22681  aalioulem2  22707  aalioulem3  22708  aalioulem4  22709  aalioulem5  22710  aaliou3lem8  22719  aaliou3lem9  22724  ulmbdd  22771  ulmcn  22772  mtest  22777  mtestbdd  22778  abelthlem2  22805  abelthlem7  22811  pilem2  22825  tanabsge  22877  cosordlem  22896  tanord  22903  logneg2  22978  abslogle  22981  dvlog2lem  23011  cxple2a  23058  abscxpbnd  23105  atans2  23240  leibpi  23251  o1cxp  23282  cxploglim2  23286  jensenlem2  23295  emcllem6  23308  harmoniclbnd  23316  harmonicubnd  23317  harmonicbnd4  23318  fsumharmonic  23319  ftalem2  23325  basellem3  23334  basellem5  23336  basellem6  23337  dvdsflsumcom  23442  fsumfldivdiaglem  23443  ppiub  23457  chtublem  23464  logfac2  23470  chpub  23473  logfacubnd  23474  logfaclbnd  23475  logfacbnd3  23476  logexprlim  23478  bcmono  23530  bpos1lem  23535  bposlem1  23537  bposlem2  23538  bposlem3  23539  bposlem4  23540  bposlem5  23541  bposlem6  23542  bposlem7  23543  bposlem9  23545  lgsdirprm  23582  lgsquadlem1  23607  2sqlem8  23625  chebbnd1lem1  23632  chebbnd1lem3  23634  chtppilimlem1  23636  chpchtlim  23642  vmadivsumb  23646  rplogsumlem1  23647  rplogsumlem2  23648  rpvmasumlem  23650  dchrisumlema  23651  dchrisumlem2  23653  dchrisumlem3  23654  dchrmusum2  23657  dchrvmasumlem2  23661  dchrvmasumlem3  23662  dchrvmasumlema  23663  dchrvmasumiflem1  23664  dchrisum0flblem1  23671  dchrisum0flblem2  23672  dchrisum0fno1  23674  dchrisum0re  23676  dchrisum0lem1b  23678  dchrisum0lem1  23679  dchrisum0lem2a  23680  dchrisum0  23683  rplogsum  23690  mudivsum  23693  mulogsumlem  23694  logdivsum  23696  mulog2sumlem1  23697  mulog2sumlem2  23698  2vmadivsumlem  23703  log2sumbnd  23707  selberglem2  23709  selbergb  23712  selberg2lem  23713  selberg2b  23715  chpdifbndlem1  23716  logdivbnd  23719  selberg3lem1  23720  selberg3lem2  23721  selberg4lem1  23723  pntrmax  23727  pntrsumo1  23728  pntrsumbnd  23729  pntrlog2bndlem1  23740  pntrlog2bndlem2  23741  pntrlog2bndlem3  23742  pntrlog2bndlem5  23744  pntrlog2bndlem6  23746  pntrlog2bnd  23747  pntpbnd1a  23748  pntpbnd1  23749  pntpbnd2  23750  pntibndlem2  23754  pntibndlem3  23755  pntlemg  23761  pntlemr  23765  pntlemj  23766  pntlemf  23768  pntlemk  23769  pntlemo  23770  pntleml  23774  abvcxp  23778  qabvle  23788  padicabv  23793  ostth2lem2  23797  ostth2lem3  23798  ostth3  23801  axlowdimlem16  24238  axcontlem8  24252  axcontlem10  24254  wwlkm1edg  24713  wwlksubclwwlk  24782  smcnlem  25585  nmoub3i  25666  ubthlem3  25766  minvecolem2  25769  minvecolem3  25770  minvecolem4  25774  htthlem  25812  bcs2  26077  pjhthlem1  26287  cnlnadjlem2  26965  cnlnadjlem7  26970  nmopadjlem  26986  nmoptrii  26991  nmopcoadji  26998  leopnmid  27035  cdj1i  27330  nndiffz1  27574  nexple  27983  esumpcvgval  28062  oddpwdc  28271  eulerpartlems  28277  eulerpartlemgc  28279  eulerpartlemb  28285  dstfrvunirn  28391  orvclteinc  28392  ballotlemsima  28432  ballotlemfrcn0  28446  signstfveq0  28512  lgamgulmlem2  28550  lgamgulmlem3  28551  lgamgulmlem5  28553  lgambdd  28557  mblfinlem2  30028  mblfinlem3  30029  mblfinlem4  30030  ismblfin  30031  itg2addnc  30045  iblmulc2nc  30056  bddiblnc  30061  ftc1anclem7  30072  ftc1anclem8  30073  filbcmb  30207  geomcau  30228  prdsbnd  30265  cntotbnd  30268  bfplem2  30295  rrntotbnd  30308  iccbnd  30312  lzunuz  30677  irrapxlem3  30736  irrapxlem4  30737  irrapxlem5  30738  pellexlem2  30742  pell1qrge1  30782  monotoddzzfi  30854  jm2.17a  30874  rmygeid  30878  fzmaxdif  30895  jm2.27c  30925  jm3.1lem1  30935  expdiophlem1  30939  isprm7  31168  dvgrat  31169  monoords  31450  absnpncan2d  31456  absnpncan3d  31461  ssfiunibd  31463  leadd12dd  31475  fmul01  31528  fmul01lt1lem1  31532  fmul01lt1lem2  31533  fprodle  31558  climsuselem1  31567  climsuse  31568  dvdivbd  31674  dvbdfbdioolem2  31680  ioodvbdlimc1lem1  31682  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvnmul  31694  dvnprodlem1  31697  dvnprodlem2  31698  iblspltprt  31726  itgspltprt  31732  stoweidlem1  31737  stoweidlem3  31739  stoweidlem5  31741  stoweidlem11  31747  stoweidlem17  31753  stoweidlem20  31756  stoweidlem26  31762  stoweidlem34  31770  wallispilem4  31804  stirlinglem11  31820  stirlinglem12  31821  stirlinglem13  31822  fourierdlem12  31855  fourierdlem15  31858  fourierdlem20  31863  fourierdlem30  31873  fourierdlem39  31882  fourierdlem42  31885  fourierdlem47  31890  fourierdlem50  31893  fourierdlem64  31907  fourierdlem65  31908  fourierdlem68  31911  fourierdlem73  31916  fourierdlem77  31920  fourierdlem79  31922  fourierdlem87  31930  elaa2lem  31970  etransclem23  31994  imo72b2lem0  37786  int-ineqtransd  37819
  Copyright terms: Public domain W3C validator