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

Theorem letrd 8973
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 8914 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <_  C )  ->  A  <_  C
) )
73, 4, 5, 6syl3anc 1182 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <_  C
)  ->  A  <_  C ) )
81, 2, 7mp2and 660 1  |-  ( ph  ->  A  <_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   class class class wbr 4023   RRcr 8736    <_ cle 8868
This theorem is referenced by:  supmul1  9719  supmul  9722  iccsplit  10768  fzdisj  10817  flwordi  10942  uzsup  10967  seqf1olem1  11085  bernneq  11227  bernneq3  11229  discr1  11237  faclbnd  11303  faclbnd4lem1  11306  facubnd  11313  seqcoll  11401  sqrlem7  11734  absle  11799  releabs  11805  absrdbnd  11825  rexuzre  11836  limsupgre  11955  lo1bddrp  11999  rlimclim1  12019  rlimresb  12039  rlimrege0  12053  o1add  12087  o1sub  12089  climsqz  12114  climsqz2  12115  rlimsqzlem  12122  rlimsqz  12123  rlimsqz2  12124  rlimno1  12127  isercoll  12141  caucvgrlem  12145  iseraltlem3  12156  o1fsum  12271  cvgcmp  12274  cvgcmpce  12276  climcnds  12310  expcnv  12322  cvgrat  12339  mertenslem2  12341  eftlub  12389  rpnnen2  12504  bitsfzo  12626  isprm5  12791  eulerthlem2  12850  pcmpt2  12941  pcfac  12947  prmreclem3  12965  prmreclem4  12966  prmreclem5  12967  4sqlem11  13002  vdwlem1  13028  vdwlem3  13030  prdsxmetlem  17932  nrmmetd  18097  nm2dif  18146  nlmvscnlem2  18196  nmoco  18246  nmotri  18248  nghmcn  18254  icccmplem2  18328  reconnlem2  18332  elii1  18433  xrhmeo  18444  cnheiborlem  18452  bndth  18456  tchcphlem1  18665  ipcnlem2  18671  cncmet  18744  minveclem2  18790  minveclem4  18796  ivthlem2  18812  ovolunlem1a  18855  ovolunlem1  18856  ovolfiniun  18860  ovoliunlem1  18861  ovolicc2lem4  18879  ovolicc2lem5  18880  ovolicopnf  18883  nulmbl2  18894  ioombl1lem4  18918  ioorcl2  18927  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  volcn  18961  vitalilem2  18964  vitali  18968  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  itg2splitlem  19103  itg2monolem1  19105  itg2monolem3  19107  itg2mono  19108  itg2cnlem1  19116  itgle  19164  bddmulibl  19193  ditgsplitlem  19210  dveflem  19326  dvlip  19340  dveq0  19347  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsum2  19381  fta1glem2  19552  dgradd2  19649  plydiveu  19678  fta1lem  19687  aalioulem2  19713  aalioulem3  19714  aalioulem4  19715  aalioulem5  19716  aaliou3lem8  19725  aaliou3lem9  19730  ulmbdd  19775  ulmcn  19776  mtest  19781  abelthlem2  19808  abelthlem7  19814  pilem2  19828  tanabsge  19874  cosordlem  19893  tanord  19900  logneg2  19969  dvlog2lem  19999  cxple2a  20046  abscxpbnd  20093  atans2  20227  leibpi  20238  o1cxp  20269  cxploglim2  20273  jensenlem2  20282  emcllem6  20294  harmoniclbnd  20302  harmonicubnd  20303  harmonicbnd4  20304  fsumharmonic  20305  ftalem2  20311  basellem3  20320  basellem5  20322  basellem6  20323  dvdsflsumcom  20428  fsumfldivdiaglem  20429  ppiub  20443  chtublem  20450  logfac2  20456  chpub  20459  logfacubnd  20460  logfaclbnd  20461  logfacbnd3  20462  logexprlim  20464  bcmono  20516  bpos1lem  20521  bposlem1  20523  bposlem2  20524  bposlem3  20525  bposlem4  20526  bposlem5  20527  bposlem6  20528  bposlem7  20529  bposlem9  20531  lgsdirprm  20568  lgsquadlem1  20593  2sqlem8  20611  chebbnd1lem1  20618  chebbnd1lem3  20620  chtppilimlem1  20622  chpchtlim  20628  vmadivsumb  20632  rplogsumlem1  20633  rplogsumlem2  20634  rpvmasumlem  20636  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  dchrmusum2  20643  dchrvmasumlem2  20647  dchrvmasumlem3  20648  dchrvmasumlema  20649  dchrvmasumiflem1  20650  dchrisum0flblem1  20657  dchrisum0flblem2  20658  dchrisum0fno1  20660  dchrisum0re  20662  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0  20669  rplogsum  20676  mudivsum  20679  mulogsumlem  20680  logdivsum  20682  mulog2sumlem1  20683  mulog2sumlem2  20684  2vmadivsumlem  20689  log2sumbnd  20693  selberglem2  20695  selbergb  20698  selberg2lem  20699  selberg2b  20701  chpdifbndlem1  20702  logdivbnd  20705  selberg3lem1  20706  selberg3lem2  20707  selberg4lem1  20709  pntrmax  20713  pntrsumo1  20714  pntrsumbnd  20715  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntrlog2bnd  20733  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2  20740  pntibndlem3  20741  pntlemg  20747  pntlemr  20751  pntlemj  20752  pntlemf  20754  pntlemk  20755  pntlemo  20756  pntleml  20760  abvcxp  20764  qabvle  20774  padicabv  20779  ostth2lem2  20783  ostth2lem3  20784  ostth3  20787  smcnlem  21270  nmoub3i  21351  ubthlem3  21451  minvecolem2  21454  minvecolem3  21455  minvecolem4  21459  htthlem  21497  bcs2  21761  pjhthlem1  21970  cnlnadjlem2  22648  cnlnadjlem7  22653  nmopadjlem  22669  nmoptrii  22674  nmopcoadji  22681  leopnmid  22718  cdj1i  23013  ballotlemsdom  23070  ballotlemsima  23074  ballotlemfrcn0  23088  esumpcvgval  23446  dstfrvunirn  23675  axlowdimlem16  24585  axcontlem8  24599  axcontlem10  24601  icccon2  25700  icccon3  25701  filbcmb  26432  trirn  26463  geomcau  26475  prdsbnd  26517  cntotbnd  26520  bfplem2  26547  rrntotbnd  26560  iccbnd  26564  lzunuz  26847  irrapxlem3  26909  irrapxlem4  26910  irrapxlem5  26911  pellexlem2  26915  pell1qrge1  26955  monotoddzzfi  27027  jm2.17a  27047  rmygeid  27051  fzmaxdif  27068  jm2.27c  27100  jm3.1lem1  27110  expdiophlem1  27114  climsuselem1  27733  climsuse  27734  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-resscn 8794  ax-pre-lttri 8811  ax-pre-lttrn 8812
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873
  Copyright terms: Public domain W3C validator