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

Theorem letrd 10073
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 10010 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
73, 4, 5, 6syl3anc 1318 . 2 (𝜑 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
81, 2, 7mp2and 711 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977   class class class wbr 4583  cr 9814  cle 9954
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959
This theorem is referenced by:  lesub3d  10524  supmul1  10869  supmul  10872  nn0negleid  11222  eluzuzle  11572  iccsplit  12176  supicc  12191  fzdisj  12239  difelfzle  12321  flwordi  12475  flleceil  12514  uzsup  12524  modltm1p1mod  12584  seqf1olem1  12702  bernneq  12852  bernneq3  12854  discr1  12862  faclbnd  12939  faclbnd4lem1  12942  facubnd  12949  seqcoll  13105  sqrlem7  13837  absle  13903  releabs  13909  absrdbnd  13929  rexuzre  13940  limsupgre  14060  lo1bddrp  14104  rlimclim1  14124  rlimresb  14144  rlimrege0  14158  o1add  14192  o1sub  14194  climsqz  14219  climsqz2  14220  rlimsqzlem  14227  rlimsqz  14228  rlimsqz2  14229  rlimno1  14232  isercoll  14246  caucvgrlem  14251  iseraltlem3  14262  o1fsum  14386  cvgcmp  14389  cvgcmpce  14391  climcnds  14422  expcnv  14435  cvgrat  14454  mertenslem2  14456  fprodle  14566  eftlub  14678  rpnnen2lem12  14793  bitsfzo  14995  isprm5  15257  isprm7  15258  eulerthlem2  15325  pcmpt2  15435  pcfac  15441  prmreclem3  15460  prmreclem4  15461  prmreclem5  15462  4sqlem11  15497  vdwlem1  15523  vdwlem3  15525  prdsxmetlem  21983  nrmmetd  22189  nm2dif  22239  nlmvscnlem2  22299  nmoco  22351  nmotri  22353  nghmcn  22359  icccmplem2  22434  reconnlem2  22438  elii1  22542  xrhmeo  22553  cnheiborlem  22561  bndth  22565  tchcphlem1  22842  ipcnlem2  22851  cncmet  22927  trirn  22991  minveclem2  23005  minveclem4  23011  ivthlem2  23028  ovolunlem1a  23071  ovolunlem1  23072  ovolfiniun  23076  ovoliunlem1  23077  ovolicc2lem4  23095  ovolicc2lem5  23096  ovolicopnf  23099  nulmbl2  23111  ioombl1lem4  23136  ioorcl2  23146  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  volcn  23180  vitalilem2  23184  vitali  23188  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  itg2splitlem  23321  itg2monolem1  23323  itg2monolem3  23325  itg2mono  23326  itg2cnlem1  23334  itgle  23382  bddmulibl  23411  ditgsplitlem  23430  dveflem  23546  dvlip  23560  dveq0  23567  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsum2  23601  fta1glem2  23730  dgradd2  23828  plydiveu  23857  fta1lem  23866  aalioulem2  23892  aalioulem3  23893  aalioulem4  23894  aalioulem5  23895  aaliou3lem8  23904  aaliou3lem9  23909  ulmbdd  23956  ulmcn  23957  mtest  23962  mtestbdd  23963  abelthlem2  23990  abelthlem7  23996  pilem2  24010  tanabsge  24062  cosordlem  24081  tanord  24088  logneg2  24165  abslogle  24168  dvlog2lem  24198  cxple2a  24245  abscxpbnd  24294  atans2  24458  leibpi  24469  o1cxp  24501  cxploglim2  24505  jensenlem2  24514  emcllem6  24527  harmoniclbnd  24535  harmonicubnd  24536  harmonicbnd4  24537  fsumharmonic  24538  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem5  24559  lgambdd  24563  ftalem2  24600  basellem3  24609  basellem5  24611  basellem6  24612  dvdsflsumcom  24714  fsumfldivdiaglem  24715  ppiub  24729  chtublem  24736  logfac2  24742  chpub  24745  logfacubnd  24746  logfaclbnd  24747  logfacbnd3  24748  logexprlim  24750  bcmono  24802  bpos1lem  24807  bposlem1  24809  bposlem2  24810  bposlem3  24811  bposlem4  24812  bposlem5  24813  bposlem6  24814  bposlem7  24815  bposlem9  24817  lgsdirprm  24856  lgsquadlem1  24905  2lgslem1c  24918  2sqlem8  24951  chebbnd1lem1  24958  chebbnd1lem3  24960  chtppilimlem1  24962  chpchtlim  24968  vmadivsumb  24972  rplogsumlem1  24973  rplogsumlem2  24974  rpvmasumlem  24976  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrvmasumlema  24989  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0fno1  25000  dchrisum0re  25002  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0  25009  rplogsum  25016  mudivsum  25019  mulogsumlem  25020  logdivsum  25022  mulog2sumlem1  25023  mulog2sumlem2  25024  2vmadivsumlem  25029  log2sumbnd  25033  selberglem2  25035  selbergb  25038  selberg2lem  25039  selberg2b  25041  chpdifbndlem1  25042  logdivbnd  25045  selberg3lem1  25046  selberg3lem2  25047  selberg4lem1  25049  pntrmax  25053  pntrsumo1  25054  pntrsumbnd  25055  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2  25080  pntibndlem3  25081  pntlemg  25087  pntlemr  25091  pntlemj  25092  pntlemf  25094  pntlemk  25095  pntlemo  25096  pntleml  25100  abvcxp  25104  qabvle  25114  padicabv  25119  ostth2lem2  25123  ostth2lem3  25124  ostth3  25127  axlowdimlem16  25637  axcontlem8  25651  axcontlem10  25653  wwlkm1edg  26263  wwlksubclwwlk  26332  smcnlem  26936  nmoub3i  27012  ubthlem3  27112  minvecolem2  27115  minvecolem3  27116  minvecolem4  27120  htthlem  27158  bcs2  27423  pjhthlem1  27634  cnlnadjlem2  28311  cnlnadjlem7  28316  nmopadjlem  28332  nmoptrii  28337  nmopcoadji  28344  leopnmid  28381  cdj1i  28676  nndiffz1  28936  pmtrto1cl  29180  psgnfzto1stlem  29181  fzto1st  29184  psgnfzto1st  29186  smatrcl  29190  submateqlem1  29201  nexple  29399  esumpcvgval  29467  oddpwdc  29743  eulerpartlems  29749  eulerpartlemgc  29751  eulerpartlemb  29757  dstfrvunirn  29863  orvclteinc  29864  ballotlemsima  29904  ballotlemfrcn0  29918  signstfveq0  29980  dnibndlem2  31639  dnibndlem6  31643  dnibndlem9  31646  dnibndlem10  31647  dnibndlem11  31648  dnibndlem12  31649  knoppcnlem4  31656  unblimceq0lem  31667  unblimceq0  31668  unbdqndv2lem2  31671  knoppndvlem11  31683  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem18  31690  knoppndvlem21  31693  poimirlem6  32585  poimirlem7  32586  poimirlem13  32592  poimirlem15  32594  poimirlem29  32608  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnc  32634  iblmulc2nc  32645  bddiblnc  32650  ftc1anclem7  32661  ftc1anclem8  32662  filbcmb  32705  geomcau  32725  prdsbnd  32762  cntotbnd  32765  bfplem2  32792  rrntotbnd  32805  iccbnd  32809  lzunuz  36349  irrapxlem3  36406  irrapxlem4  36407  irrapxlem5  36408  pellexlem2  36412  pell1qrge1  36452  monotoddzzfi  36525  jm2.17a  36545  rmygeid  36549  fzmaxdif  36566  jm2.27c  36592  jm3.1lem1  36602  expdiophlem1  36606  imo72b2lem0  37487  int-ineqtransd  37519  dvgrat  37533  monoords  38452  absnpncan2d  38457  absnpncan3d  38462  ssfiunibd  38464  leadd12dd  38473  sqrlearg  38627  fmul01  38647  fmul01lt1lem1  38651  fmul01lt1lem2  38652  climsuselem1  38674  climsuse  38675  dvdivbd  38813  dvbdfbdioolem2  38819  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmul  38833  dvnprodlem1  38836  dvnprodlem2  38837  iblspltprt  38865  itgspltprt  38871  stoweidlem1  38894  stoweidlem3  38896  stoweidlem5  38898  stoweidlem11  38904  stoweidlem17  38910  stoweidlem20  38913  stoweidlem26  38919  stoweidlem34  38927  wallispilem4  38961  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  fourierdlem12  39012  fourierdlem15  39015  fourierdlem20  39020  fourierdlem30  39030  fourierdlem39  39039  fourierdlem42  39042  fourierdlem47  39046  fourierdlem50  39049  fourierdlem64  39063  fourierdlem65  39064  fourierdlem68  39067  fourierdlem73  39072  fourierdlem77  39076  fourierdlem79  39078  fourierdlem87  39086  elaa2lem  39126  etransclem23  39150  ioorrnopnlem  39200  salgencntex  39237  sge0le  39300  sge0isum  39320  sge0xaddlem1  39326  hoicvr  39438  hsphoidmvle2  39475  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem4  39488  hspmbllem1  39516  hspmbllem2  39517  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  lighneallem4a  40063  wwlksm1edg  41078  wwlksubclwwlks  41232  fllog2  42160
  Copyright terms: Public domain W3C validator