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

Theorem letrd 10790
Description: Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.)
Hypotheses
Ref Expression
ltd.1 (𝜑𝐴 ∈ ℝ)
ltd.2 (𝜑𝐵 ∈ ℝ)
letrd.3 (𝜑𝐶 ∈ ℝ)
letrd.4 (𝜑𝐴𝐵)
letrd.5 (𝜑𝐵𝐶)
Assertion
Ref Expression
letrd (𝜑𝐴𝐶)

Proof of Theorem letrd
StepHypRef Expression
1 letrd.4 . 2 (𝜑𝐴𝐵)
2 letrd.5 . 2 (𝜑𝐵𝐶)
3 ltd.1 . . 3 (𝜑𝐴 ∈ ℝ)
4 ltd.2 . . 3 (𝜑𝐵 ∈ ℝ)
5 letrd.3 . . 3 (𝜑𝐶 ∈ ℝ)
6 letr 10727 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
73, 4, 5, 6syl3anc 1368 . 2 (𝜑 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
81, 2, 7mp2and 698 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112   class class class wbr 5033  cr 10529  cle 10669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-resscn 10587  ax-pre-lttri 10604  ax-pre-lttrn 10605
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674
This theorem is referenced by:  lesub3d  11251  supmul1  11601  supmul  11604  nn0negleid  11941  eluzuzle  12244  iccsplit  12867  supicc  12883  fzdisj  12933  ssfzunsnext  12951  difelfzle  13019  flwordi  13181  flleceil  13220  uzsup  13230  modltm1p1mod  13290  seqf1olem1  13409  bernneq  13590  bernneq3  13592  discr1  13600  faclbnd  13650  faclbnd4lem1  13653  facubnd  13660  seqcoll  13822  sqrlem7  14603  absle  14670  releabs  14676  absrdbnd  14696  rexuzre  14707  limsupgre  14833  lo1bddrp  14877  rlimclim1  14897  rlimresb  14917  rlimrege0  14931  o1add  14965  o1sub  14967  climsqz  14992  climsqz2  14993  rlimsqzlem  15000  rlimsqz  15001  rlimsqz2  15002  rlimno1  15005  isercoll  15019  caucvgrlem  15024  iseraltlem3  15035  o1fsum  15163  cvgcmp  15166  cvgcmpce  15168  climcnds  15201  expcnv  15214  cvgrat  15234  mertenslem2  15236  fprodle  15345  eftlub  15457  rpnnen2lem12  15573  bitsfzo  15777  isprm5  16044  isprm7  16045  eulerthlem2  16112  pcmpt2  16222  pcfac  16228  prmreclem3  16247  prmreclem4  16248  prmreclem5  16249  4sqlem11  16284  vdwlem1  16310  vdwlem3  16312  setsstruct2  16516  prdsxmetlem  22978  nrmmetd  23184  nm2dif  23234  nlmvscnlem2  23294  nmoco  23346  nmotri  23348  nghmcn  23354  icccmplem2  23431  reconnlem2  23435  elii1  23543  xrhmeo  23554  cnheiborlem  23562  bndth  23566  tcphcphlem1  23842  ipcnlem2  23851  cncmet  23929  trirn  24007  minveclem2  24033  minveclem4  24039  ivthlem2  24059  ovolunlem1a  24103  ovolunlem1  24104  ovolfiniun  24108  ovoliunlem1  24109  ovolicc2lem4  24127  ovolicc2lem5  24128  ovolicopnf  24131  nulmbl2  24143  ioombl1lem4  24168  ioorcl2  24179  uniioombllem3  24192  uniioombllem4  24193  uniioombllem5  24194  volcn  24213  vitalilem2  24216  vitali  24220  mbfi1fseqlem5  24326  mbfi1fseqlem6  24327  itg2splitlem  24355  itg2monolem1  24357  itg2monolem3  24359  itg2mono  24360  itg2cnlem1  24368  itgle  24416  bddmulibl  24445  bddiblnc  24448  ditgsplitlem  24466  dveflem  24585  dvlip  24599  dveq0  24606  dvfsumabs  24629  dvfsumlem1  24632  dvfsumlem2  24633  dvfsumlem3  24634  dvfsumlem4  24635  dvfsum2  24640  fta1glem2  24770  dgradd2  24868  plydiveu  24897  fta1lem  24906  aalioulem2  24932  aalioulem3  24933  aalioulem4  24934  aalioulem5  24935  aaliou3lem8  24944  aaliou3lem9  24949  ulmbdd  24996  ulmcn  24997  mtest  25002  mtestbdd  25003  abelthlem2  25030  abelthlem7  25036  pilem2  25050  tanabsge  25102  cosordlem  25125  tanord  25133  logneg2  25209  abslogle  25212  dvlog2lem  25246  cxple2a  25293  abscxpbnd  25345  atans2  25520  leibpi  25531  o1cxp  25563  cxploglim2  25567  jensenlem2  25576  emcllem6  25589  harmoniclbnd  25597  harmonicubnd  25598  harmonicbnd4  25599  fsumharmonic  25600  lgamgulmlem2  25618  lgamgulmlem3  25619  lgamgulmlem5  25621  lgambdd  25625  ftalem2  25662  basellem3  25671  basellem5  25673  basellem6  25674  dvdsflsumcom  25776  fsumfldivdiaglem  25777  ppiub  25791  chtublem  25798  logfac2  25804  chpub  25807  logfacubnd  25808  logfaclbnd  25809  logfacbnd3  25810  logexprlim  25812  bcmono  25864  bpos1lem  25869  bposlem1  25871  bposlem2  25872  bposlem3  25873  bposlem4  25874  bposlem5  25875  bposlem6  25876  bposlem7  25877  bposlem9  25879  lgsdirprm  25918  lgsquadlem1  25967  2lgslem1c  25980  2sqlem8  26013  chebbnd1lem1  26056  chebbnd1lem3  26058  chtppilimlem1  26060  chpchtlim  26066  vmadivsumb  26070  rplogsumlem1  26071  rplogsumlem2  26072  rpvmasumlem  26074  dchrisumlema  26075  dchrisumlem2  26077  dchrisumlem3  26078  dchrmusum2  26081  dchrvmasumlem2  26085  dchrvmasumlem3  26086  dchrvmasumlema  26087  dchrvmasumiflem1  26088  dchrisum0flblem1  26095  dchrisum0flblem2  26096  dchrisum0fno1  26098  dchrisum0re  26100  dchrisum0lem1b  26102  dchrisum0lem1  26103  dchrisum0lem2a  26104  dchrisum0  26107  rplogsum  26114  mudivsum  26117  mulogsumlem  26118  logdivsum  26120  mulog2sumlem1  26121  mulog2sumlem2  26122  2vmadivsumlem  26127  log2sumbnd  26131  selberglem2  26133  selbergb  26136  selberg2lem  26137  selberg2b  26139  chpdifbndlem1  26140  logdivbnd  26143  selberg3lem1  26144  selberg3lem2  26145  selberg4lem1  26147  pntrmax  26151  pntrsumo1  26152  pntrsumbnd  26153  pntrlog2bndlem1  26164  pntrlog2bndlem2  26165  pntrlog2bndlem3  26166  pntrlog2bndlem5  26168  pntrlog2bndlem6  26170  pntrlog2bnd  26171  pntpbnd1a  26172  pntpbnd1  26173  pntpbnd2  26174  pntibndlem2  26178  pntibndlem3  26179  pntlemg  26185  pntlemr  26189  pntlemj  26190  pntlemf  26192  pntlemk  26193  pntlemo  26194  pntleml  26198  abvcxp  26202  qabvle  26212  padicabv  26217  ostth2lem2  26221  ostth2lem3  26222  ostth3  26225  axlowdimlem16  26754  axcontlem8  26768  axcontlem10  26770  wwlksm1edg  27670  wwlksubclwwlk  27846  smcnlem  28483  nmoub3i  28559  ubthlem3  28658  minvecolem2  28661  minvecolem3  28662  minvecolem4  28666  htthlem  28703  bcs2  28968  pjhthlem1  29177  cnlnadjlem2  29854  cnlnadjlem7  29859  nmopadjlem  29875  nmoptrii  29880  nmopcoadji  29887  leopnmid  29924  cdj1i  30219  nndiffz1  30538  pmtrto1cl  30794  psgnfzto1stlem  30795  fzto1st  30798  psgnfzto1st  30800  cyc3conja  30852  smatrcl  31149  submateqlem1  31160  nexple  31376  esumpcvgval  31445  oddpwdc  31720  eulerpartlems  31726  eulerpartlemgc  31728  eulerpartlemb  31734  dstfrvunirn  31840  orvclteinc  31841  ballotlemsima  31881  ballotlemfrcn0  31895  signstfveq0  31955  fsum2dsub  31986  breprexplemc  32011  breprexp  32012  logdivsqrle  32029  hgt750lemb  32035  hgt750leme  32037  tgoldbachgnn  32038  dnibndlem2  33926  dnibndlem6  33930  dnibndlem9  33933  dnibndlem10  33934  dnibndlem11  33935  dnibndlem12  33936  knoppcnlem4  33943  unblimceq0lem  33953  unblimceq0  33954  unbdqndv2lem2  33957  knoppndvlem11  33969  knoppndvlem14  33972  knoppndvlem15  33973  knoppndvlem18  33976  knoppndvlem21  33979  poimirlem6  35056  poimirlem7  35057  poimirlem13  35063  poimirlem15  35065  poimirlem29  35079  mblfinlem2  35088  mblfinlem3  35089  mblfinlem4  35090  ismblfin  35091  itg2addnc  35104  iblmulc2nc  35115  ftc1anclem7  35129  ftc1anclem8  35130  filbcmb  35171  geomcau  35190  prdsbnd  35224  cntotbnd  35227  bfplem2  35254  rrntotbnd  35267  iccbnd  35271  lcmineqlem20  39329  lcmineqlem21  39330  lcmineqlem22  39331  3lexlogpow5ineq2  39335  2np3bcnp1  39339  metakunt1  39341  metakunt12  39352  metakunt28  39368  lzunuz  39696  irrapxlem3  39752  irrapxlem4  39753  irrapxlem5  39754  pellexlem2  39758  pell1qrge1  39798  monotoddzzfi  39870  jm2.17a  39888  rmygeid  39892  fzmaxdif  39909  jm2.27c  39935  jm3.1lem1  39945  expdiophlem1  39949  imo72b2lem0  40856  int-ineqtransd  40887  dvgrat  41003  monoords  41916  absnpncan2d  41921  absnpncan3d  41926  ssfiunibd  41928  leadd12dd  41935  rexabslelem  42042  uzublem  42054  sqrlearg  42177  fmul01  42209  fmul01lt1lem1  42213  fmul01lt1lem2  42214  climsuselem1  42236  climsuse  42237  limsupresico  42329  limsupubuzlem  42341  limsupmnfuzlem  42355  limsupre3uzlem  42364  liminfresico  42400  limsup10exlem  42401  cnrefiisplem  42458  dvdivbd  42552  dvbdfbdioolem2  42558  ioodvbdlimc1lem1  42560  ioodvbdlimc1lem2  42561  ioodvbdlimc2lem  42563  dvnmul  42572  dvnprodlem1  42575  dvnprodlem2  42576  iblspltprt  42602  itgspltprt  42608  stoweidlem1  42630  stoweidlem3  42632  stoweidlem5  42634  stoweidlem11  42640  stoweidlem17  42646  stoweidlem20  42649  stoweidlem26  42655  stoweidlem34  42663  wallispilem4  42697  stirlinglem11  42713  stirlinglem12  42714  stirlinglem13  42715  fourierdlem12  42748  fourierdlem15  42751  fourierdlem20  42756  fourierdlem30  42766  fourierdlem39  42775  fourierdlem42  42778  fourierdlem47  42782  fourierdlem50  42785  fourierdlem64  42799  fourierdlem65  42800  fourierdlem68  42803  fourierdlem73  42808  fourierdlem77  42812  fourierdlem79  42814  fourierdlem87  42822  elaa2lem  42862  etransclem23  42886  ioorrnopnlem  42933  salgencntex  42970  sge0le  43033  sge0isum  43053  sge0xaddlem1  43059  hoicvr  43174  hsphoidmvle2  43211  hoidmv1lelem1  43217  hoidmv1lelem2  43218  hoidmv1lelem3  43219  hoidmvlelem1  43221  hoidmvlelem2  43222  hoidmvlelem4  43224  hspmbllem1  43252  hspmbllem2  43253  smfmullem1  43410  smfmullem2  43411  smfmullem3  43412  smfsuplem1  43429  lighneallem4a  44113  fllog2  44969  itcovalt2lem2lem1  45074
  Copyright terms: Public domain W3C validator