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

Theorem letrd 9629
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 9569 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <_  C )  ->  A  <_  C
) )
73, 4, 5, 6syl3anc 1219 . 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 1758   class class class wbr 4390   RRcr 9382    <_ cle 9520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-resscn 9440  ax-pre-lttri 9457  ax-pre-lttrn 9458
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525
This theorem is referenced by:  supmul1  10396  supmul  10399  iccsplit  11519  supicc  11534  fzdisj  11577  flwordi  11761  flleceil  11793  uzsup  11803  modltm1p1mod  11852  seqf1olem1  11946  bernneq  12091  bernneq3  12093  discr1  12101  faclbnd  12167  faclbnd4lem1  12170  facubnd  12177  seqcoll  12318  swrdn0  12426  sqrlem7  12840  absle  12905  releabs  12911  absrdbnd  12931  rexuzre  12942  limsupgre  13061  lo1bddrp  13105  rlimclim1  13125  rlimresb  13145  rlimrege0  13159  o1add  13193  o1sub  13195  climsqz  13220  climsqz2  13221  rlimsqzlem  13228  rlimsqz  13229  rlimsqz2  13230  rlimno1  13233  isercoll  13247  caucvgrlem  13252  iseraltlem3  13263  o1fsum  13378  cvgcmp  13381  cvgcmpce  13383  climcnds  13416  expcnv  13428  cvgrat  13445  mertenslem2  13447  eftlub  13495  rpnnen2  13610  bitsfzo  13733  isprm5  13900  eulerthlem2  13959  pcmpt2  14057  pcfac  14063  prmreclem3  14081  prmreclem4  14082  prmreclem5  14083  4sqlem11  14118  vdwlem1  14144  vdwlem3  14146  prdsxmetlem  20059  nrmmetd  20283  nm2dif  20332  nlmvscnlem2  20382  nmoco  20432  nmotri  20434  nghmcn  20440  icccmplem2  20516  reconnlem2  20520  elii1  20623  xrhmeo  20634  cnheiborlem  20642  bndth  20646  tchcphlem1  20866  ipcnlem2  20872  cncmet  20949  trirn  21015  minveclem2  21029  minveclem4  21035  ivthlem2  21052  ovolunlem1a  21095  ovolunlem1  21096  ovolfiniun  21100  ovoliunlem1  21101  ovolicc2lem4  21119  ovolicc2lem5  21120  ovolicopnf  21123  nulmbl2  21134  ioombl1lem4  21158  ioorcl2  21168  uniioombllem3  21181  uniioombllem4  21182  uniioombllem5  21183  volcn  21202  vitalilem2  21205  vitali  21209  mbfi1fseqlem5  21313  mbfi1fseqlem6  21314  itg2splitlem  21342  itg2monolem1  21344  itg2monolem3  21346  itg2mono  21347  itg2cnlem1  21355  itgle  21403  bddmulibl  21432  ditgsplitlem  21451  dveflem  21567  dvlip  21581  dveq0  21588  dvfsumabs  21611  dvfsumlem1  21614  dvfsumlem2  21615  dvfsumlem3  21616  dvfsumlem4  21617  dvfsum2  21622  fta1glem2  21754  dgradd2  21851  plydiveu  21880  fta1lem  21889  aalioulem2  21915  aalioulem3  21916  aalioulem4  21917  aalioulem5  21918  aaliou3lem8  21927  aaliou3lem9  21932  ulmbdd  21979  ulmcn  21980  mtest  21985  mtestbdd  21986  abelthlem2  22013  abelthlem7  22019  pilem2  22033  tanabsge  22084  cosordlem  22103  tanord  22110  logneg2  22180  abslogle  22183  dvlog2lem  22213  cxple2a  22260  abscxpbnd  22307  atans2  22442  leibpi  22453  o1cxp  22484  cxploglim2  22488  jensenlem2  22497  emcllem6  22510  harmoniclbnd  22518  harmonicubnd  22519  harmonicbnd4  22520  fsumharmonic  22521  ftalem2  22527  basellem3  22536  basellem5  22538  basellem6  22539  dvdsflsumcom  22644  fsumfldivdiaglem  22645  ppiub  22659  chtublem  22666  logfac2  22672  chpub  22675  logfacubnd  22676  logfaclbnd  22677  logfacbnd3  22678  logexprlim  22680  bcmono  22732  bpos1lem  22737  bposlem1  22739  bposlem2  22740  bposlem3  22741  bposlem4  22742  bposlem5  22743  bposlem6  22744  bposlem7  22745  bposlem9  22747  lgsdirprm  22784  lgsquadlem1  22809  2sqlem8  22827  chebbnd1lem1  22834  chebbnd1lem3  22836  chtppilimlem1  22838  chpchtlim  22844  vmadivsumb  22848  rplogsumlem1  22849  rplogsumlem2  22850  rpvmasumlem  22852  dchrisumlema  22853  dchrisumlem2  22855  dchrisumlem3  22856  dchrmusum2  22859  dchrvmasumlem2  22863  dchrvmasumlem3  22864  dchrvmasumlema  22865  dchrvmasumiflem1  22866  dchrisum0flblem1  22873  dchrisum0flblem2  22874  dchrisum0fno1  22876  dchrisum0re  22878  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0  22885  rplogsum  22892  mudivsum  22895  mulogsumlem  22896  logdivsum  22898  mulog2sumlem1  22899  mulog2sumlem2  22900  2vmadivsumlem  22905  log2sumbnd  22909  selberglem2  22911  selbergb  22914  selberg2lem  22915  selberg2b  22917  chpdifbndlem1  22918  logdivbnd  22921  selberg3lem1  22922  selberg3lem2  22923  selberg4lem1  22925  pntrmax  22929  pntrsumo1  22930  pntrsumbnd  22931  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntpbnd1a  22950  pntpbnd1  22951  pntpbnd2  22952  pntibndlem2  22956  pntibndlem3  22957  pntlemg  22963  pntlemr  22967  pntlemj  22968  pntlemf  22970  pntlemk  22971  pntlemo  22972  pntleml  22976  abvcxp  22980  qabvle  22990  padicabv  22995  ostth2lem2  22999  ostth2lem3  23000  ostth3  23003  axlowdimlem16  23338  axcontlem8  23352  axcontlem10  23354  smcnlem  24227  nmoub3i  24308  ubthlem3  24408  minvecolem2  24411  minvecolem3  24412  minvecolem4  24416  htthlem  24454  bcs2  24719  pjhthlem1  24929  cnlnadjlem2  25607  cnlnadjlem7  25612  nmopadjlem  25628  nmoptrii  25633  nmopcoadji  25640  leopnmid  25677  cdj1i  25972  nndiffz1  26209  nexple  26582  esumpcvgval  26661  oddpwdc  26871  eulerpartlems  26877  eulerpartlemgc  26879  eulerpartlemb  26885  dstfrvunirn  26991  orvclteinc  26992  ballotlemsima  27032  ballotlemfrcn0  27046  signstfveq0  27112  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem5  27153  lgambdd  27157  mblfinlem2  28567  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  itg2addnc  28584  iblmulc2nc  28595  bddiblnc  28600  ftc1anclem7  28611  ftc1anclem8  28612  filbcmb  28772  geomcau  28793  prdsbnd  28830  cntotbnd  28833  bfplem2  28860  rrntotbnd  28873  iccbnd  28877  lzunuz  29244  irrapxlem3  29303  irrapxlem4  29304  irrapxlem5  29305  pellexlem2  29309  pell1qrge1  29349  monotoddzzfi  29421  jm2.17a  29441  rmygeid  29445  fzmaxdif  29462  jm2.27c  29494  jm3.1lem1  29504  expdiophlem1  29508  fmul01  29899  fmul01lt1lem1  29903  fmul01lt1lem2  29904  climsuselem1  29918  climsuse  29919  stoweidlem1  29934  stoweidlem3  29936  stoweidlem5  29938  stoweidlem11  29944  stoweidlem17  29950  stoweidlem20  29953  stoweidlem26  29959  stoweidlem34  29967  wallispilem4  30001  stirlinglem11  30017  stirlinglem12  30018  stirlinglem13  30019  wwlkm1edg  30505  wwlksubclwwlk  30604  difelfzle  30625
  Copyright terms: Public domain W3C validator