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

Theorem letrd 9520
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 9460 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <_  C )  ->  A  <_  C
) )
73, 4, 5, 6syl3anc 1218 . 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 1756   class class class wbr 4287   RRcr 9273    <_ cle 9411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-pre-lttri 9348  ax-pre-lttrn 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416
This theorem is referenced by:  supmul1  10287  supmul  10290  iccsplit  11410  supicc  11425  fzdisj  11468  flwordi  11652  flleceil  11684  uzsup  11694  modltm1p1mod  11743  seqf1olem1  11837  bernneq  11982  bernneq3  11984  discr1  11992  faclbnd  12058  faclbnd4lem1  12061  facubnd  12068  seqcoll  12208  swrdn0  12316  sqrlem7  12730  absle  12795  releabs  12801  absrdbnd  12821  rexuzre  12832  limsupgre  12951  lo1bddrp  12995  rlimclim1  13015  rlimresb  13035  rlimrege0  13049  o1add  13083  o1sub  13085  climsqz  13110  climsqz2  13111  rlimsqzlem  13118  rlimsqz  13119  rlimsqz2  13120  rlimno1  13123  isercoll  13137  caucvgrlem  13142  iseraltlem3  13153  o1fsum  13268  cvgcmp  13271  cvgcmpce  13273  climcnds  13306  expcnv  13318  cvgrat  13335  mertenslem2  13337  eftlub  13385  rpnnen2  13500  bitsfzo  13623  isprm5  13790  eulerthlem2  13849  pcmpt2  13947  pcfac  13953  prmreclem3  13971  prmreclem4  13972  prmreclem5  13973  4sqlem11  14008  vdwlem1  14034  vdwlem3  14036  prdsxmetlem  19918  nrmmetd  20142  nm2dif  20191  nlmvscnlem2  20241  nmoco  20291  nmotri  20293  nghmcn  20299  icccmplem2  20375  reconnlem2  20379  elii1  20482  xrhmeo  20493  cnheiborlem  20501  bndth  20505  tchcphlem1  20725  ipcnlem2  20731  cncmet  20808  trirn  20874  minveclem2  20888  minveclem4  20894  ivthlem2  20911  ovolunlem1a  20954  ovolunlem1  20955  ovolfiniun  20959  ovoliunlem1  20960  ovolicc2lem4  20978  ovolicc2lem5  20979  ovolicopnf  20982  nulmbl2  20993  ioombl1lem4  21017  ioorcl2  21027  uniioombllem3  21040  uniioombllem4  21041  uniioombllem5  21042  volcn  21061  vitalilem2  21064  vitali  21068  mbfi1fseqlem5  21172  mbfi1fseqlem6  21173  itg2splitlem  21201  itg2monolem1  21203  itg2monolem3  21205  itg2mono  21206  itg2cnlem1  21214  itgle  21262  bddmulibl  21291  ditgsplitlem  21310  dveflem  21426  dvlip  21440  dveq0  21447  dvfsumabs  21470  dvfsumlem1  21473  dvfsumlem2  21474  dvfsumlem3  21475  dvfsumlem4  21476  dvfsum2  21481  fta1glem2  21613  dgradd2  21710  plydiveu  21739  fta1lem  21748  aalioulem2  21774  aalioulem3  21775  aalioulem4  21776  aalioulem5  21777  aaliou3lem8  21786  aaliou3lem9  21791  ulmbdd  21838  ulmcn  21839  mtest  21844  mtestbdd  21845  abelthlem2  21872  abelthlem7  21878  pilem2  21892  tanabsge  21943  cosordlem  21962  tanord  21969  logneg2  22039  abslogle  22042  dvlog2lem  22072  cxple2a  22119  abscxpbnd  22166  atans2  22301  leibpi  22312  o1cxp  22343  cxploglim2  22347  jensenlem2  22356  emcllem6  22369  harmoniclbnd  22377  harmonicubnd  22378  harmonicbnd4  22379  fsumharmonic  22380  ftalem2  22386  basellem3  22395  basellem5  22397  basellem6  22398  dvdsflsumcom  22503  fsumfldivdiaglem  22504  ppiub  22518  chtublem  22525  logfac2  22531  chpub  22534  logfacubnd  22535  logfaclbnd  22536  logfacbnd3  22537  logexprlim  22539  bcmono  22591  bpos1lem  22596  bposlem1  22598  bposlem2  22599  bposlem3  22600  bposlem4  22601  bposlem5  22602  bposlem6  22603  bposlem7  22604  bposlem9  22606  lgsdirprm  22643  lgsquadlem1  22668  2sqlem8  22686  chebbnd1lem1  22693  chebbnd1lem3  22695  chtppilimlem1  22697  chpchtlim  22703  vmadivsumb  22707  rplogsumlem1  22708  rplogsumlem2  22709  rpvmasumlem  22711  dchrisumlema  22712  dchrisumlem2  22714  dchrisumlem3  22715  dchrmusum2  22718  dchrvmasumlem2  22722  dchrvmasumlem3  22723  dchrvmasumlema  22724  dchrvmasumiflem1  22725  dchrisum0flblem1  22732  dchrisum0flblem2  22733  dchrisum0fno1  22735  dchrisum0re  22737  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2a  22741  dchrisum0  22744  rplogsum  22751  mudivsum  22754  mulogsumlem  22755  logdivsum  22757  mulog2sumlem1  22758  mulog2sumlem2  22759  2vmadivsumlem  22764  log2sumbnd  22768  selberglem2  22770  selbergb  22773  selberg2lem  22774  selberg2b  22776  chpdifbndlem1  22777  logdivbnd  22780  selberg3lem1  22781  selberg3lem2  22782  selberg4lem1  22784  pntrmax  22788  pntrsumo1  22789  pntrsumbnd  22790  pntrlog2bndlem1  22801  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem5  22805  pntrlog2bndlem6  22807  pntrlog2bnd  22808  pntpbnd1a  22809  pntpbnd1  22810  pntpbnd2  22811  pntibndlem2  22815  pntibndlem3  22816  pntlemg  22822  pntlemr  22826  pntlemj  22827  pntlemf  22829  pntlemk  22830  pntlemo  22831  pntleml  22835  abvcxp  22839  qabvle  22849  padicabv  22854  ostth2lem2  22858  ostth2lem3  22859  ostth3  22862  axlowdimlem16  23154  axcontlem8  23168  axcontlem10  23170  smcnlem  24043  nmoub3i  24124  ubthlem3  24224  minvecolem2  24227  minvecolem3  24228  minvecolem4  24232  htthlem  24270  bcs2  24535  pjhthlem1  24745  cnlnadjlem2  25423  cnlnadjlem7  25428  nmopadjlem  25444  nmoptrii  25449  nmopcoadji  25456  leopnmid  25493  cdj1i  25788  nndiffz1  26026  nexple  26400  esumpcvgval  26479  oddpwdc  26689  eulerpartlems  26695  eulerpartlemgc  26697  eulerpartlemb  26703  dstfrvunirn  26809  orvclteinc  26810  ballotlemsima  26850  ballotlemfrcn0  26864  signstfveq0  26930  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem5  26971  lgambdd  26975  mblfinlem2  28382  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  itg2addnc  28399  iblmulc2nc  28410  bddiblnc  28415  ftc1anclem7  28426  ftc1anclem8  28427  filbcmb  28587  geomcau  28608  prdsbnd  28645  cntotbnd  28648  bfplem2  28675  rrntotbnd  28688  iccbnd  28692  lzunuz  29059  irrapxlem3  29118  irrapxlem4  29119  irrapxlem5  29120  pellexlem2  29124  pell1qrge1  29164  monotoddzzfi  29236  jm2.17a  29256  rmygeid  29260  fzmaxdif  29277  jm2.27c  29309  jm3.1lem1  29319  expdiophlem1  29323  fmul01  29714  fmul01lt1lem1  29718  fmul01lt1lem2  29719  climsuselem1  29733  climsuse  29734  stoweidlem1  29749  stoweidlem3  29751  stoweidlem5  29753  stoweidlem11  29759  stoweidlem17  29765  stoweidlem20  29768  stoweidlem26  29774  stoweidlem34  29782  wallispilem4  29816  stirlinglem11  29832  stirlinglem12  29833  stirlinglem13  29834  wwlkm1edg  30320  wwlksubclwwlk  30419  difelfzle  30440
  Copyright terms: Public domain W3C validator