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

Theorem letrd 10395
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 10332 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
73, 4, 5, 6syl3anc 1475 . 2 (𝜑 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
81, 2, 7mp2and 671 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2144   class class class wbr 4784  cr 10136  cle 10276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-resscn 10194  ax-pre-lttri 10211  ax-pre-lttrn 10212
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-nel 3046  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-er 7895  df-en 8109  df-dom 8110  df-sdom 8111  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281
This theorem is referenced by:  lesub3d  10846  supmul1  11193  supmul  11196  nn0negleid  11546  eluzuzle  11896  iccsplit  12511  supicc  12526  fzdisj  12574  ssfzunsnext  12592  difelfzle  12659  flwordi  12820  flleceil  12859  uzsup  12869  modltm1p1mod  12929  seqf1olem1  13046  bernneq  13196  bernneq3  13198  discr1  13206  faclbnd  13280  faclbnd4lem1  13283  facubnd  13290  seqcoll  13449  sqrlem7  14196  absle  14262  releabs  14268  absrdbnd  14288  rexuzre  14299  limsupgre  14419  lo1bddrp  14463  rlimclim1  14483  rlimresb  14503  rlimrege0  14517  o1add  14551  o1sub  14553  climsqz  14578  climsqz2  14579  rlimsqzlem  14586  rlimsqz  14587  rlimsqz2  14588  rlimno1  14591  isercoll  14605  caucvgrlem  14610  iseraltlem3  14621  o1fsum  14751  cvgcmp  14754  cvgcmpce  14756  climcnds  14789  expcnv  14802  cvgrat  14821  mertenslem2  14823  fprodle  14932  eftlub  15044  rpnnen2lem12  15159  bitsfzo  15364  isprm5  15625  isprm7  15626  eulerthlem2  15693  pcmpt2  15803  pcfac  15809  prmreclem3  15828  prmreclem4  15829  prmreclem5  15830  4sqlem11  15865  vdwlem1  15891  vdwlem3  15893  setsstruct2  16102  prdsxmetlem  22392  nrmmetd  22598  nm2dif  22648  nlmvscnlem2  22708  nmoco  22760  nmotri  22762  nghmcn  22768  icccmplem2  22845  reconnlem2  22849  elii1  22953  xrhmeo  22964  cnheiborlem  22972  bndth  22976  tchcphlem1  23252  ipcnlem2  23261  cncmet  23337  trirn  23401  minveclem2  23415  minveclem4  23421  ivthlem2  23439  ovolunlem1a  23483  ovolunlem1  23484  ovolfiniun  23488  ovoliunlem1  23489  ovolicc2lem4  23507  ovolicc2lem5  23508  ovolicopnf  23511  nulmbl2  23523  ioombl1lem4  23548  ioorcl2  23559  uniioombllem3  23572  uniioombllem4  23573  uniioombllem5  23574  volcn  23593  vitalilem2  23596  vitali  23600  mbfi1fseqlem5  23705  mbfi1fseqlem6  23706  itg2splitlem  23734  itg2monolem1  23736  itg2monolem3  23738  itg2mono  23739  itg2cnlem1  23747  itgle  23795  bddmulibl  23824  ditgsplitlem  23843  dveflem  23961  dvlip  23975  dveq0  23982  dvfsumabs  24005  dvfsumlem1  24008  dvfsumlem2  24009  dvfsumlem3  24010  dvfsumlem4  24011  dvfsum2  24016  fta1glem2  24145  dgradd2  24243  plydiveu  24272  fta1lem  24281  aalioulem2  24307  aalioulem3  24308  aalioulem4  24309  aalioulem5  24310  aaliou3lem8  24319  aaliou3lem9  24324  ulmbdd  24371  ulmcn  24372  mtest  24377  mtestbdd  24378  abelthlem2  24405  abelthlem7  24411  pilem2  24425  tanabsge  24478  cosordlem  24497  tanord  24504  logneg2  24581  abslogle  24584  dvlog2lem  24618  cxple2a  24665  abscxpbnd  24714  atans2  24878  leibpi  24889  o1cxp  24921  cxploglim2  24925  jensenlem2  24934  emcllem6  24947  harmoniclbnd  24955  harmonicubnd  24956  harmonicbnd4  24957  fsumharmonic  24958  lgamgulmlem2  24976  lgamgulmlem3  24977  lgamgulmlem5  24979  lgambdd  24983  ftalem2  25020  basellem3  25029  basellem5  25031  basellem6  25032  dvdsflsumcom  25134  fsumfldivdiaglem  25135  ppiub  25149  chtublem  25156  logfac2  25162  chpub  25165  logfacubnd  25166  logfaclbnd  25167  logfacbnd3  25168  logexprlim  25170  bcmono  25222  bpos1lem  25227  bposlem1  25229  bposlem2  25230  bposlem3  25231  bposlem4  25232  bposlem5  25233  bposlem6  25234  bposlem7  25235  bposlem9  25237  lgsdirprm  25276  lgsquadlem1  25325  2lgslem1c  25338  2sqlem8  25371  chebbnd1lem1  25378  chebbnd1lem3  25380  chtppilimlem1  25382  chpchtlim  25388  vmadivsumb  25392  rplogsumlem1  25393  rplogsumlem2  25394  rpvmasumlem  25396  dchrisumlema  25397  dchrisumlem2  25399  dchrisumlem3  25400  dchrmusum2  25403  dchrvmasumlem2  25407  dchrvmasumlem3  25408  dchrvmasumlema  25409  dchrvmasumiflem1  25410  dchrisum0flblem1  25417  dchrisum0flblem2  25418  dchrisum0fno1  25420  dchrisum0re  25422  dchrisum0lem1b  25424  dchrisum0lem1  25425  dchrisum0lem2a  25426  dchrisum0  25429  rplogsum  25436  mudivsum  25439  mulogsumlem  25440  logdivsum  25442  mulog2sumlem1  25443  mulog2sumlem2  25444  2vmadivsumlem  25449  log2sumbnd  25453  selberglem2  25455  selbergb  25458  selberg2lem  25459  selberg2b  25461  chpdifbndlem1  25462  logdivbnd  25465  selberg3lem1  25466  selberg3lem2  25467  selberg4lem1  25469  pntrmax  25473  pntrsumo1  25474  pntrsumbnd  25475  pntrlog2bndlem1  25486  pntrlog2bndlem2  25487  pntrlog2bndlem3  25488  pntrlog2bndlem5  25490  pntrlog2bndlem6  25492  pntrlog2bnd  25493  pntpbnd1a  25494  pntpbnd1  25495  pntpbnd2  25496  pntibndlem2  25500  pntibndlem3  25501  pntlemg  25507  pntlemr  25511  pntlemj  25512  pntlemf  25514  pntlemk  25515  pntlemo  25516  pntleml  25520  abvcxp  25524  qabvle  25534  padicabv  25539  ostth2lem2  25543  ostth2lem3  25544  ostth3  25547  axlowdimlem16  26057  axcontlem8  26071  axcontlem10  26073  wwlksm1edg  27014  wwlksubclwwlk  27213  smcnlem  27886  nmoub3i  27962  ubthlem3  28062  minvecolem2  28065  minvecolem3  28066  minvecolem4  28070  htthlem  28108  bcs2  28373  pjhthlem1  28584  cnlnadjlem2  29261  cnlnadjlem7  29266  nmopadjlem  29282  nmoptrii  29287  nmopcoadji  29294  leopnmid  29331  cdj1i  29626  nndiffz1  29882  pmtrto1cl  30183  psgnfzto1stlem  30184  fzto1st  30187  psgnfzto1st  30189  smatrcl  30196  submateqlem1  30207  nexple  30405  esumpcvgval  30474  oddpwdc  30750  eulerpartlems  30756  eulerpartlemgc  30758  eulerpartlemb  30764  dstfrvunirn  30870  orvclteinc  30871  ballotlemsima  30911  ballotlemfrcn0  30925  signstfveq0  30988  fsum2dsub  31019  breprexplemc  31044  breprexp  31045  logdivsqrle  31062  hgt750lemb  31068  hgt750leme  31070  tgoldbachgnn  31071  dnibndlem2  32800  dnibndlem6  32804  dnibndlem9  32807  dnibndlem10  32808  dnibndlem11  32809  dnibndlem12  32810  knoppcnlem4  32817  unblimceq0lem  32828  unblimceq0  32829  unbdqndv2lem2  32832  knoppndvlem11  32844  knoppndvlem14  32847  knoppndvlem15  32848  knoppndvlem18  32851  knoppndvlem21  32854  poimirlem6  33741  poimirlem7  33742  poimirlem13  33748  poimirlem15  33750  poimirlem29  33764  mblfinlem2  33773  mblfinlem3  33774  mblfinlem4  33775  ismblfin  33776  itg2addnc  33789  iblmulc2nc  33800  bddiblnc  33805  ftc1anclem7  33816  ftc1anclem8  33817  filbcmb  33860  geomcau  33880  prdsbnd  33917  cntotbnd  33920  bfplem2  33947  rrntotbnd  33960  iccbnd  33964  lzunuz  37850  irrapxlem3  37907  irrapxlem4  37908  irrapxlem5  37909  pellexlem2  37913  pell1qrge1  37953  monotoddzzfi  38026  jm2.17a  38046  rmygeid  38050  fzmaxdif  38067  jm2.27c  38093  jm3.1lem1  38103  expdiophlem1  38107  imo72b2lem0  38984  int-ineqtransd  39016  dvgrat  39030  monoords  40022  absnpncan2d  40027  absnpncan3d  40032  ssfiunibd  40034  leadd12dd  40042  rexabslelem  40155  uzublem  40167  sqrlearg  40292  fmul01  40324  fmul01lt1lem1  40328  fmul01lt1lem2  40329  climsuselem1  40351  climsuse  40352  limsupresico  40444  limsupubuzlem  40456  limsupmnfuzlem  40470  limsupre3uzlem  40479  liminfresico  40515  limsup10exlem  40516  cnrefiisplem  40567  dvdivbd  40650  dvbdfbdioolem2  40656  ioodvbdlimc1lem1  40658  ioodvbdlimc1lem2  40659  ioodvbdlimc2lem  40661  dvnmul  40670  dvnprodlem1  40673  dvnprodlem2  40674  iblspltprt  40700  itgspltprt  40706  stoweidlem1  40729  stoweidlem3  40731  stoweidlem5  40733  stoweidlem11  40739  stoweidlem17  40745  stoweidlem20  40748  stoweidlem26  40754  stoweidlem34  40762  wallispilem4  40796  stirlinglem11  40812  stirlinglem12  40813  stirlinglem13  40814  fourierdlem12  40847  fourierdlem15  40850  fourierdlem20  40855  fourierdlem30  40865  fourierdlem39  40874  fourierdlem42  40877  fourierdlem47  40881  fourierdlem50  40884  fourierdlem64  40898  fourierdlem65  40899  fourierdlem68  40902  fourierdlem73  40907  fourierdlem77  40911  fourierdlem79  40913  fourierdlem87  40921  elaa2lem  40961  etransclem23  40985  ioorrnopnlem  41035  salgencntex  41072  sge0le  41135  sge0isum  41155  sge0xaddlem1  41161  hoicvr  41276  hsphoidmvle2  41313  hoidmv1lelem1  41319  hoidmv1lelem2  41320  hoidmv1lelem3  41321  hoidmvlelem1  41323  hoidmvlelem2  41324  hoidmvlelem4  41326  hspmbllem1  41354  hspmbllem2  41355  smfmullem1  41512  smfmullem2  41513  smfmullem3  41514  smfsuplem1  41531  lighneallem4a  42043  fllog2  42880
  Copyright terms: Public domain W3C validator