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

Theorem letrd 10232
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 10169 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
73, 4, 5, 6syl3anc 1366 . 2 (𝜑 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
81, 2, 7mp2and 715 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030   class class class wbr 4685  cr 9973  cle 10113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-pre-lttri 10048  ax-pre-lttrn 10049
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118
This theorem is referenced by:  lesub3d  10683  supmul1  11030  supmul  11033  nn0negleid  11383  eluzuzle  11734  iccsplit  12343  supicc  12358  fzdisj  12406  ssfzunsnext  12424  difelfzle  12491  flwordi  12653  flleceil  12692  uzsup  12702  modltm1p1mod  12762  seqf1olem1  12880  bernneq  13030  bernneq3  13032  discr1  13040  faclbnd  13117  faclbnd4lem1  13120  facubnd  13127  seqcoll  13286  sqrlem7  14033  absle  14099  releabs  14105  absrdbnd  14125  rexuzre  14136  limsupgre  14256  lo1bddrp  14300  rlimclim1  14320  rlimresb  14340  rlimrege0  14354  o1add  14388  o1sub  14390  climsqz  14415  climsqz2  14416  rlimsqzlem  14423  rlimsqz  14424  rlimsqz2  14425  rlimno1  14428  isercoll  14442  caucvgrlem  14447  iseraltlem3  14458  o1fsum  14589  cvgcmp  14592  cvgcmpce  14594  climcnds  14627  expcnv  14640  cvgrat  14659  mertenslem2  14661  fprodle  14771  eftlub  14883  rpnnen2lem12  14998  bitsfzo  15204  isprm5  15466  isprm7  15467  eulerthlem2  15534  pcmpt2  15644  pcfac  15650  prmreclem3  15669  prmreclem4  15670  prmreclem5  15671  4sqlem11  15706  vdwlem1  15732  vdwlem3  15734  setsstruct2  15943  prdsxmetlem  22220  nrmmetd  22426  nm2dif  22476  nlmvscnlem2  22536  nmoco  22588  nmotri  22590  nghmcn  22596  icccmplem2  22673  reconnlem2  22677  elii1  22781  xrhmeo  22792  cnheiborlem  22800  bndth  22804  tchcphlem1  23080  ipcnlem2  23089  cncmet  23165  trirn  23229  minveclem2  23243  minveclem4  23249  ivthlem2  23267  ovolunlem1a  23310  ovolunlem1  23311  ovolfiniun  23315  ovoliunlem1  23316  ovolicc2lem4  23334  ovolicc2lem5  23335  ovolicopnf  23338  nulmbl2  23350  ioombl1lem4  23375  ioorcl2  23386  uniioombllem3  23399  uniioombllem4  23400  uniioombllem5  23401  volcn  23420  vitalilem2  23423  vitali  23427  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  itg2splitlem  23560  itg2monolem1  23562  itg2monolem3  23564  itg2mono  23565  itg2cnlem1  23573  itgle  23621  bddmulibl  23650  ditgsplitlem  23669  dveflem  23787  dvlip  23801  dveq0  23808  dvfsumabs  23831  dvfsumlem1  23834  dvfsumlem2  23835  dvfsumlem3  23836  dvfsumlem4  23837  dvfsum2  23842  fta1glem2  23971  dgradd2  24069  plydiveu  24098  fta1lem  24107  aalioulem2  24133  aalioulem3  24134  aalioulem4  24135  aalioulem5  24136  aaliou3lem8  24145  aaliou3lem9  24150  ulmbdd  24197  ulmcn  24198  mtest  24203  mtestbdd  24204  abelthlem2  24231  abelthlem7  24237  pilem2  24251  tanabsge  24303  cosordlem  24322  tanord  24329  logneg2  24406  abslogle  24409  dvlog2lem  24443  cxple2a  24490  abscxpbnd  24539  atans2  24703  leibpi  24714  o1cxp  24746  cxploglim2  24750  jensenlem2  24759  emcllem6  24772  harmoniclbnd  24780  harmonicubnd  24781  harmonicbnd4  24782  fsumharmonic  24783  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem5  24804  lgambdd  24808  ftalem2  24845  basellem3  24854  basellem5  24856  basellem6  24857  dvdsflsumcom  24959  fsumfldivdiaglem  24960  ppiub  24974  chtublem  24981  logfac2  24987  chpub  24990  logfacubnd  24991  logfaclbnd  24992  logfacbnd3  24993  logexprlim  24995  bcmono  25047  bpos1lem  25052  bposlem1  25054  bposlem2  25055  bposlem3  25056  bposlem4  25057  bposlem5  25058  bposlem6  25059  bposlem7  25060  bposlem9  25062  lgsdirprm  25101  lgsquadlem1  25150  2lgslem1c  25163  2sqlem8  25196  chebbnd1lem1  25203  chebbnd1lem3  25205  chtppilimlem1  25207  chpchtlim  25213  vmadivsumb  25217  rplogsumlem1  25218  rplogsumlem2  25219  rpvmasumlem  25221  dchrisumlema  25222  dchrisumlem2  25224  dchrisumlem3  25225  dchrmusum2  25228  dchrvmasumlem2  25232  dchrvmasumlem3  25233  dchrvmasumlema  25234  dchrvmasumiflem1  25235  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0fno1  25245  dchrisum0re  25247  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0  25254  rplogsum  25261  mudivsum  25264  mulogsumlem  25265  logdivsum  25267  mulog2sumlem1  25268  mulog2sumlem2  25269  2vmadivsumlem  25274  log2sumbnd  25278  selberglem2  25280  selbergb  25283  selberg2lem  25284  selberg2b  25286  chpdifbndlem1  25287  logdivbnd  25290  selberg3lem1  25291  selberg3lem2  25292  selberg4lem1  25294  pntrmax  25298  pntrsumo1  25299  pntrsumbnd  25300  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntrlog2bnd  25318  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntibndlem2  25325  pntibndlem3  25326  pntlemg  25332  pntlemr  25336  pntlemj  25337  pntlemf  25339  pntlemk  25340  pntlemo  25341  pntleml  25345  abvcxp  25349  qabvle  25359  padicabv  25364  ostth2lem2  25368  ostth2lem3  25369  ostth3  25372  axlowdimlem16  25882  axcontlem8  25896  axcontlem10  25898  wwlksm1edg  26835  wwlksubclwwlk  27023  smcnlem  27680  nmoub3i  27756  ubthlem3  27856  minvecolem2  27859  minvecolem3  27860  minvecolem4  27864  htthlem  27902  bcs2  28167  pjhthlem1  28378  cnlnadjlem2  29055  cnlnadjlem7  29060  nmopadjlem  29076  nmoptrii  29081  nmopcoadji  29088  leopnmid  29125  cdj1i  29420  nndiffz1  29676  pmtrto1cl  29977  psgnfzto1stlem  29978  fzto1st  29981  psgnfzto1st  29983  smatrcl  29990  submateqlem1  30001  nexple  30199  esumpcvgval  30268  oddpwdc  30544  eulerpartlems  30550  eulerpartlemgc  30552  eulerpartlemb  30558  dstfrvunirn  30664  orvclteinc  30665  ballotlemsima  30705  ballotlemfrcn0  30719  signstfveq0  30782  fsum2dsub  30813  breprexplemc  30838  breprexp  30839  logdivsqrle  30856  hgt750lemb  30862  hgt750leme  30864  tgoldbachgnn  30865  dnibndlem2  32594  dnibndlem6  32598  dnibndlem9  32601  dnibndlem10  32602  dnibndlem11  32603  dnibndlem12  32604  knoppcnlem4  32611  unblimceq0lem  32622  unblimceq0  32623  unbdqndv2lem2  32626  knoppndvlem11  32638  knoppndvlem14  32641  knoppndvlem15  32642  knoppndvlem18  32645  knoppndvlem21  32648  poimirlem6  33545  poimirlem7  33546  poimirlem13  33552  poimirlem15  33554  poimirlem29  33568  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2addnc  33594  iblmulc2nc  33605  bddiblnc  33610  ftc1anclem7  33621  ftc1anclem8  33622  filbcmb  33665  geomcau  33685  prdsbnd  33722  cntotbnd  33725  bfplem2  33752  rrntotbnd  33765  iccbnd  33769  lzunuz  37648  irrapxlem3  37705  irrapxlem4  37706  irrapxlem5  37707  pellexlem2  37711  pell1qrge1  37751  monotoddzzfi  37824  jm2.17a  37844  rmygeid  37848  fzmaxdif  37865  jm2.27c  37891  jm3.1lem1  37901  expdiophlem1  37905  imo72b2lem0  38782  int-ineqtransd  38814  dvgrat  38828  monoords  39825  absnpncan2d  39830  absnpncan3d  39835  ssfiunibd  39837  leadd12dd  39845  rexabslelem  39958  uzublem  39970  sqrlearg  40098  fmul01  40130  fmul01lt1lem1  40134  fmul01lt1lem2  40135  climsuselem1  40157  climsuse  40158  limsupresico  40250  limsupubuzlem  40262  limsupmnfuzlem  40276  limsupre3uzlem  40285  liminfresico  40321  limsup10exlem  40322  cnrefiisplem  40373  dvdivbd  40456  dvbdfbdioolem2  40462  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  iblspltprt  40507  itgspltprt  40513  stoweidlem1  40536  stoweidlem3  40538  stoweidlem5  40540  stoweidlem11  40546  stoweidlem17  40552  stoweidlem20  40555  stoweidlem26  40561  stoweidlem34  40569  wallispilem4  40603  stirlinglem11  40619  stirlinglem12  40620  stirlinglem13  40621  fourierdlem12  40654  fourierdlem15  40657  fourierdlem20  40662  fourierdlem30  40672  fourierdlem39  40681  fourierdlem42  40684  fourierdlem47  40688  fourierdlem50  40691  fourierdlem64  40705  fourierdlem65  40706  fourierdlem68  40709  fourierdlem73  40714  fourierdlem77  40718  fourierdlem79  40720  fourierdlem87  40728  elaa2lem  40768  etransclem23  40792  ioorrnopnlem  40842  salgencntex  40879  sge0le  40942  sge0isum  40962  sge0xaddlem1  40968  hoicvr  41083  hsphoidmvle2  41120  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem4  41133  hspmbllem1  41161  hspmbllem2  41162  smfmullem1  41319  smfmullem2  41320  smfmullem3  41321  smfsuplem1  41338  lighneallem4a  41850  fllog2  42687
  Copyright terms: Public domain W3C validator