Theorem letrd 11115

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

Step	Hyp	Ref	Expression
1		letrd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		letrd.5	. 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		letr 11052	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
7	3, 4, 5, 6	syl3anc 1369	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
8	1, 2, 7	mp2and 695	1 ⊢ (𝜑 → 𝐴 ≤ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5078  ℝcr 10854   ≤ cle 10994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-resscn 10912  ax-pre-lttri 10929  ax-pre-lttrn 10930

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-er 8472  df-en 8708  df-dom 8709  df-sdom 8710  df-pnf 10995  df-mnf 10996  df-xr 10997  df-ltxr 10998  df-le 10999

This theorem is referenced by:  lesub3d  11576  supmul1  11927  supmul  11930  nn0negleid  12268  eluzuzle  12573  iccsplit  13199  supicc  13215  fzdisj  13265  ssfzunsnext  13283  difelfzle  13351  flwordi  13513  flleceil  13554  uzsup  13564  modltm1p1mod  13624  seqf1olem1  13743  bernneq  13925  bernneq3  13927  discr1  13935  faclbnd  13985  faclbnd4lem1  13988  facubnd  13995  seqcoll  14159  sqrlem7  14941  absle  15008  releabs  15014  absrdbnd  15034  rexuzre  15045  limsupgre  15171  lo1bddrp  15215  rlimclim1  15235  rlimresb  15255  rlimrege0  15269  o1add  15304  o1sub  15306  climsqz  15331  climsqz2  15332  rlimsqzlem  15341  rlimsqz  15342  rlimsqz2  15343  rlimno1  15346  isercoll  15360  caucvgrlem  15365  iseraltlem3  15376  o1fsum  15506  cvgcmp  15509  cvgcmpce  15511  climcnds  15544  expcnv  15557  cvgrat  15576  mertenslem2  15578  fprodle  15687  eftlub  15799  rpnnen2lem12  15915  bitsfzo  16123  isprm5  16393  isprm7  16394  eulerthlem2  16464  pcmpt2  16575  pcfac  16581  prmreclem3  16600  prmreclem4  16601  prmreclem5  16602  4sqlem11  16637  vdwlem1  16663  vdwlem3  16665  setsstruct2  16856  prdsxmetlem  23502  nrmmetd  23711  nm2dif  23762  nlmvscnlem2  23830  nmoco  23882  nmotri  23884  nghmcn  23890  icccmplem2  23967  reconnlem2  23971  elii1  24079  xrhmeo  24090  cnheiborlem  24098  bndth  24102  tcphcphlem1  24380  ipcnlem2  24389  cncmet  24467  trirn  24545  minveclem2  24571  minveclem4  24577  ivthlem2  24597  ovolunlem1a  24641  ovolunlem1  24642  ovolfiniun  24646  ovoliunlem1  24647  ovolicc2lem4  24665  ovolicc2lem5  24666  ovolicopnf  24669  nulmbl2  24681  ioombl1lem4  24706  ioorcl2  24717  uniioombllem3  24730  uniioombllem4  24731  uniioombllem5  24732  volcn  24751  vitalilem2  24754  vitali  24758  mbfi1fseqlem5  24865  mbfi1fseqlem6  24866  itg2splitlem  24894  itg2monolem1  24896  itg2monolem3  24898  itg2mono  24899  itg2cnlem1  24907  itgle  24955  bddmulibl  24984  bddiblnc  24987  ditgsplitlem  25005  dveflem  25124  dvlip  25138  dveq0  25145  dvfsumabs  25168  dvfsumlem1  25171  dvfsumlem2  25172  dvfsumlem3  25173  dvfsumlem4  25174  dvfsum2  25179  fta1glem2  25312  dgradd2  25410  plydiveu  25439  fta1lem  25448  aalioulem2  25474  aalioulem3  25475  aalioulem4  25476  aalioulem5  25477  aaliou3lem8  25486  aaliou3lem9  25491  ulmbdd  25538  ulmcn  25539  mtest  25544  mtestbdd  25545  abelthlem2  25572  abelthlem7  25578  pilem2  25592  tanabsge  25644  cosordlem  25667  tanord  25675  logneg2  25751  abslogle  25754  dvlog2lem  25788  cxple2a  25835  abscxpbnd  25887  atans2  26062  leibpi  26073  o1cxp  26105  cxploglim2  26109  jensenlem2  26118  emcllem6  26131  harmoniclbnd  26139  harmonicubnd  26140  harmonicbnd4  26141  fsumharmonic  26142  lgamgulmlem2  26160  lgamgulmlem3  26161  lgamgulmlem5  26163  lgambdd  26167  ftalem2  26204  basellem3  26213  basellem5  26215  basellem6  26216  dvdsflsumcom  26318  fsumfldivdiaglem  26319  ppiub  26333  chtublem  26340  logfac2  26346  chpub  26349  logfacubnd  26350  logfaclbnd  26351  logfacbnd3  26352  logexprlim  26354  bcmono  26406  bpos1lem  26411  bposlem1  26413  bposlem2  26414  bposlem3  26415  bposlem4  26416  bposlem5  26417  bposlem6  26418  bposlem7  26419  bposlem9  26421  lgsdirprm  26460  lgsquadlem1  26509  2lgslem1c  26522  2sqlem8  26555  chebbnd1lem1  26598  chebbnd1lem3  26600  chtppilimlem1  26602  chpchtlim  26608  vmadivsumb  26612  rplogsumlem1  26613  rplogsumlem2  26614  rpvmasumlem  26616  dchrisumlema  26617  dchrisumlem2  26619  dchrisumlem3  26620  dchrmusum2  26623  dchrvmasumlem2  26627  dchrvmasumlem3  26628  dchrvmasumlema  26629  dchrvmasumiflem1  26630  dchrisum0flblem1  26637  dchrisum0flblem2  26638  dchrisum0fno1  26640  dchrisum0re  26642  dchrisum0lem1b  26644  dchrisum0lem1  26645  dchrisum0lem2a  26646  dchrisum0  26649  rplogsum  26656  mudivsum  26659  mulogsumlem  26660  logdivsum  26662  mulog2sumlem1  26663  mulog2sumlem2  26664  2vmadivsumlem  26669  log2sumbnd  26673  selberglem2  26675  selbergb  26678  selberg2lem  26679  selberg2b  26681  chpdifbndlem1  26682  logdivbnd  26685  selberg3lem1  26686  selberg3lem2  26687  selberg4lem1  26689  pntrmax  26693  pntrsumo1  26694  pntrsumbnd  26695  pntrlog2bndlem1  26706  pntrlog2bndlem2  26707  pntrlog2bndlem3  26708  pntrlog2bndlem5  26710  pntrlog2bndlem6  26712  pntrlog2bnd  26713  pntpbnd1a  26714  pntpbnd1  26715  pntpbnd2  26716  pntibndlem2  26720  pntibndlem3  26721  pntlemg  26727  pntlemr  26731  pntlemj  26732  pntlemf  26734  pntlemk  26735  pntlemo  26736  pntleml  26740  abvcxp  26744  qabvle  26754  padicabv  26759  ostth2lem2  26763  ostth2lem3  26764  ostth3  26767  axlowdimlem16  27306  axcontlem8  27320  axcontlem10  27322  wwlksm1edg  28225  wwlksubclwwlk  28401  smcnlem  29038  nmoub3i  29114  ubthlem3  29213  minvecolem2  29216  minvecolem3  29217  minvecolem4  29221  htthlem  29258  bcs2  29523  pjhthlem1  29732  cnlnadjlem2  30409  cnlnadjlem7  30414  nmopadjlem  30430  nmoptrii  30435  nmopcoadji  30442  leopnmid  30479  cdj1i  30774  nndiffz1  31086  pmtrto1cl  31345  psgnfzto1stlem  31346  fzto1st  31349  psgnfzto1st  31351  cyc3conja  31403  smatrcl  31725  submateqlem1  31736  nexple  31956  esumpcvgval  32025  oddpwdc  32300  eulerpartlems  32306  eulerpartlemgc  32308  eulerpartlemb  32314  dstfrvunirn  32420  orvclteinc  32421  ballotlemsima  32461  ballotlemfrcn0  32475  signstfveq0  32535  fsum2dsub  32566  breprexplemc  32591  breprexp  32592  logdivsqrle  32609  hgt750lemb  32615  hgt750leme  32617  tgoldbachgnn  32618  dnibndlem2  34638  dnibndlem6  34642  dnibndlem9  34645  dnibndlem10  34646  dnibndlem11  34647  dnibndlem12  34648  knoppcnlem4  34655  unblimceq0lem  34665  unblimceq0  34666  unbdqndv2lem2  34669  knoppndvlem11  34681  knoppndvlem14  34684  knoppndvlem15  34685  knoppndvlem18  34688  knoppndvlem21  34691  poimirlem6  35762  poimirlem7  35763  poimirlem13  35769  poimirlem15  35771  poimirlem29  35785  mblfinlem2  35794  mblfinlem3  35795  mblfinlem4  35796  ismblfin  35797  itg2addnc  35810  iblmulc2nc  35821  ftc1anclem7  35835  ftc1anclem8  35836  filbcmb  35877  geomcau  35896  prdsbnd  35930  cntotbnd  35933  bfplem2  35960  rrntotbnd  35973  iccbnd  35977  lcmineqlem20  40036  lcmineqlem21  40037  lcmineqlem22  40038  3lexlogpow5ineq2  40043  3lexlogpow5ineq5  40048  aks4d1p1p2  40058  aks4d1p1p4  40059  aks4d1p1p7  40062  aks4d1p1p5  40063  aks4d1p1  40064  aks4d1p2  40065  aks4d1p3  40066  aks4d1p5  40068  aks4d1p6  40069  aks4d1p7d1  40070  aks4d1p7  40071  aks4d1p8  40075  2np3bcnp1  40080  sticksstones6  40087  sticksstones7  40088  sticksstones10  40091  sticksstones12a  40093  sticksstones12  40094  sticksstones22  40104  metakunt1  40105  metakunt12  40116  metakunt28  40132  lzunuz  40570  irrapxlem3  40626  irrapxlem4  40627  irrapxlem5  40628  pellexlem2  40632  pell1qrge1  40672  monotoddzzfi  40744  jm2.17a  40762  rmygeid  40766  fzmaxdif  40783  jm2.27c  40809  jm3.1lem1  40819  expdiophlem1  40823  imo72b2lem0  41729  int-ineqtransd  41758  dvgrat  41883  monoords  42790  absnpncan2d  42795  absnpncan3d  42800  ssfiunibd  42802  leadd12dd  42809  rexabslelem  42912  uzublem  42924  sqrlearg  43045  fmul01  43075  fmul01lt1lem1  43079  fmul01lt1lem2  43080  climsuselem1  43102  climsuse  43103  limsupresico  43195  limsupubuzlem  43207  limsupmnfuzlem  43221  limsupre3uzlem  43230  liminfresico  43266  limsup10exlem  43267  cnrefiisplem  43324  dvdivbd  43418  dvbdfbdioolem2  43424  ioodvbdlimc1lem1  43426  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  dvnmul  43438  dvnprodlem1  43441  dvnprodlem2  43442  iblspltprt  43468  itgspltprt  43474  stoweidlem1  43496  stoweidlem3  43498  stoweidlem5  43500  stoweidlem11  43506  stoweidlem17  43512  stoweidlem20  43515  stoweidlem26  43521  stoweidlem34  43529  wallispilem4  43563  stirlinglem11  43579  stirlinglem12  43580  stirlinglem13  43581  fourierdlem12  43614  fourierdlem15  43617  fourierdlem20  43622  fourierdlem30  43632  fourierdlem39  43641  fourierdlem42  43644  fourierdlem47  43648  fourierdlem50  43651  fourierdlem64  43665  fourierdlem65  43666  fourierdlem68  43669  fourierdlem73  43674  fourierdlem77  43678  fourierdlem79  43680  fourierdlem87  43688  elaa2lem  43728  etransclem23  43752  ioorrnopnlem  43799  salgencntex  43836  sge0le  43899  sge0isum  43919  sge0xaddlem1  43925  hoicvr  44040  hsphoidmvle2  44077  hoidmv1lelem1  44083  hoidmv1lelem2  44084  hoidmv1lelem3  44085  hoidmvlelem1  44087  hoidmvlelem2  44088  hoidmvlelem4  44090  hspmbllem1  44118  hspmbllem2  44119  smfmullem1  44276  smfmullem2  44277  smfmullem3  44278  smfsuplem1  44295  lighneallem4a  45012  fllog2  45866  itcovalt2lem2lem1  45971