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

Theorem letrd 9227
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 9167 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <_  C )  ->  A  <_  C
) )
73, 4, 5, 6syl3anc 1184 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <_  C
)  ->  A  <_  C ) )
81, 2, 7mp2and 661 1  |-  ( ph  ->  A  <_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   class class class wbr 4212   RRcr 8989    <_ cle 9121
This theorem is referenced by:  supmul1  9973  supmul  9976  iccsplit  11029  fzdisj  11078  flwordi  11219  uzsup  11244  seqf1olem1  11362  bernneq  11505  bernneq3  11507  discr1  11515  faclbnd  11581  faclbnd4lem1  11584  facubnd  11591  seqcoll  11712  sqrlem7  12054  absle  12119  releabs  12125  absrdbnd  12145  rexuzre  12156  limsupgre  12275  lo1bddrp  12319  rlimclim1  12339  rlimresb  12359  rlimrege0  12373  o1add  12407  o1sub  12409  climsqz  12434  climsqz2  12435  rlimsqzlem  12442  rlimsqz  12443  rlimsqz2  12444  rlimno1  12447  isercoll  12461  caucvgrlem  12466  iseraltlem3  12477  o1fsum  12592  cvgcmp  12595  cvgcmpce  12597  climcnds  12631  expcnv  12643  cvgrat  12660  mertenslem2  12662  eftlub  12710  rpnnen2  12825  bitsfzo  12947  isprm5  13112  eulerthlem2  13171  pcmpt2  13262  pcfac  13268  prmreclem3  13286  prmreclem4  13287  prmreclem5  13288  4sqlem11  13323  vdwlem1  13349  vdwlem3  13351  prdsxmetlem  18398  nrmmetd  18622  nm2dif  18671  nlmvscnlem2  18721  nmoco  18771  nmotri  18773  nghmcn  18779  icccmplem2  18854  reconnlem2  18858  elii1  18960  xrhmeo  18971  cnheiborlem  18979  bndth  18983  tchcphlem1  19192  ipcnlem2  19198  cncmet  19275  minveclem2  19327  minveclem4  19333  ivthlem2  19349  ovolunlem1a  19392  ovolunlem1  19393  ovolfiniun  19397  ovoliunlem1  19398  ovolicc2lem4  19416  ovolicc2lem5  19417  ovolicopnf  19420  nulmbl2  19431  ioombl1lem4  19455  ioorcl2  19464  uniioombllem3  19477  uniioombllem4  19478  uniioombllem5  19479  volcn  19498  vitalilem2  19501  vitali  19505  mbfi1fseqlem5  19611  mbfi1fseqlem6  19612  itg2splitlem  19640  itg2monolem1  19642  itg2monolem3  19644  itg2mono  19645  itg2cnlem1  19653  itgle  19701  bddmulibl  19730  ditgsplitlem  19747  dveflem  19863  dvlip  19877  dveq0  19884  dvfsumabs  19907  dvfsumlem1  19910  dvfsumlem2  19911  dvfsumlem3  19912  dvfsumlem4  19913  dvfsum2  19918  fta1glem2  20089  dgradd2  20186  plydiveu  20215  fta1lem  20224  aalioulem2  20250  aalioulem3  20251  aalioulem4  20252  aalioulem5  20253  aaliou3lem8  20262  aaliou3lem9  20267  ulmbdd  20314  ulmcn  20315  mtest  20320  mtestbdd  20321  abelthlem2  20348  abelthlem7  20354  pilem2  20368  tanabsge  20414  cosordlem  20433  tanord  20440  logneg2  20510  abslogle  20513  dvlog2lem  20543  cxple2a  20590  abscxpbnd  20637  atans2  20771  leibpi  20782  o1cxp  20813  cxploglim2  20817  jensenlem2  20826  emcllem6  20839  harmoniclbnd  20847  harmonicubnd  20848  harmonicbnd4  20849  fsumharmonic  20850  ftalem2  20856  basellem3  20865  basellem5  20867  basellem6  20868  dvdsflsumcom  20973  fsumfldivdiaglem  20974  ppiub  20988  chtublem  20995  logfac2  21001  chpub  21004  logfacubnd  21005  logfaclbnd  21006  logfacbnd3  21007  logexprlim  21009  bcmono  21061  bpos1lem  21066  bposlem1  21068  bposlem2  21069  bposlem3  21070  bposlem4  21071  bposlem5  21072  bposlem6  21073  bposlem7  21074  bposlem9  21076  lgsdirprm  21113  lgsquadlem1  21138  2sqlem8  21156  chebbnd1lem1  21163  chebbnd1lem3  21165  chtppilimlem1  21167  chpchtlim  21173  vmadivsumb  21177  rplogsumlem1  21178  rplogsumlem2  21179  rpvmasumlem  21181  dchrisumlema  21182  dchrisumlem2  21184  dchrisumlem3  21185  dchrmusum2  21188  dchrvmasumlem2  21192  dchrvmasumlem3  21193  dchrvmasumlema  21194  dchrvmasumiflem1  21195  dchrisum0flblem1  21202  dchrisum0flblem2  21203  dchrisum0fno1  21205  dchrisum0re  21207  dchrisum0lem1b  21209  dchrisum0lem1  21210  dchrisum0lem2a  21211  dchrisum0  21214  rplogsum  21221  mudivsum  21224  mulogsumlem  21225  logdivsum  21227  mulog2sumlem1  21228  mulog2sumlem2  21229  2vmadivsumlem  21234  log2sumbnd  21238  selberglem2  21240  selbergb  21243  selberg2lem  21244  selberg2b  21246  chpdifbndlem1  21247  logdivbnd  21250  selberg3lem1  21251  selberg3lem2  21252  selberg4lem1  21254  pntrmax  21258  pntrsumo1  21259  pntrsumbnd  21260  pntrlog2bndlem1  21271  pntrlog2bndlem2  21272  pntrlog2bndlem3  21273  pntrlog2bndlem5  21275  pntrlog2bndlem6  21277  pntrlog2bnd  21278  pntpbnd1a  21279  pntpbnd1  21280  pntpbnd2  21281  pntibndlem2  21285  pntibndlem3  21286  pntlemg  21292  pntlemr  21296  pntlemj  21297  pntlemf  21299  pntlemk  21300  pntlemo  21301  pntleml  21305  abvcxp  21309  qabvle  21319  padicabv  21324  ostth2lem2  21328  ostth2lem3  21329  ostth3  21332  smcnlem  22193  nmoub3i  22274  ubthlem3  22374  minvecolem2  22377  minvecolem3  22378  minvecolem4  22382  htthlem  22420  bcs2  22684  pjhthlem1  22893  cnlnadjlem2  23571  cnlnadjlem7  23576  nmopadjlem  23592  nmoptrii  23597  nmopcoadji  23604  leopnmid  23641  cdj1i  23936  esumpcvgval  24468  dstfrvunirn  24732  orvclteinc  24733  ballotlemsima  24773  ballotlemfrcn0  24787  lgamgulmlem2  24814  lgamgulmlem3  24815  lgamgulmlem5  24817  lgambdd  24821  axlowdimlem16  25896  axcontlem8  25910  axcontlem10  25912  mblfinlem2  26244  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  itg2addnc  26259  iblmulc2nc  26270  bddiblnc  26275  ftc1anclem7  26286  ftc1anclem8  26287  filbcmb  26442  trirn  26457  geomcau  26465  prdsbnd  26502  cntotbnd  26505  bfplem2  26532  rrntotbnd  26545  iccbnd  26549  lzunuz  26826  irrapxlem3  26887  irrapxlem4  26888  irrapxlem5  26889  pellexlem2  26893  pell1qrge1  26933  monotoddzzfi  27005  jm2.17a  27025  rmygeid  27029  fzmaxdif  27046  jm2.27c  27078  jm3.1lem1  27088  expdiophlem1  27092  fmul01  27686  fmul01lt1lem1  27690  fmul01lt1lem2  27691  climsuselem1  27709  climsuse  27710  stoweidlem1  27726  stoweidlem3  27728  stoweidlem5  27730  stoweidlem11  27736  stoweidlem17  27742  stoweidlem20  27745  stoweidlem26  27751  stoweidlem34  27759  wallispilem4  27793  stirlinglem11  27809  stirlinglem12  27810  stirlinglem13  27811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-resscn 9047  ax-pre-lttri 9064  ax-pre-lttrn 9065
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-mpt 4268  df-id 4498  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-er 6905  df-en 7110  df-dom 7111  df-sdom 7112  df-pnf 9122  df-mnf 9123  df-xr 9124  df-ltxr 9125  df-le 9126
  Copyright terms: Public domain W3C validator