Theorem letrd 11340

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 11277	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
7	3, 4, 5, 6	syl3anc 1390	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
8	1, 2, 7	mp2and 709	1 ⊢ (𝜑 → 𝐴 ≤ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142   class class class wbr 5100  ℝcr 11072   ≤ cle 11217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-pre-lttri 11147  ax-pre-lttrn 11148

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222

This theorem is referenced by:  lesub3d  11805  le2addd  11806  supmul1  12161  supmul  12164  nn0negleid  12533  eluzuzle  12848  iccsplit  13489  supicc  13505  fzdisj  13556  ssfzunsnext  13574  difelfzle  13646  flwordi  13822  flleceil  13863  uzsup  13873  modltm1p1mod  13936  seqf1olem1  14054  zzlesq  14219  bernneq  14242  bernneq3  14244  discr1  14252  faclbnd  14303  faclbnd4lem1  14306  facubnd  14313  seqcoll  14477  01sqrexlem7  15275  absle  15343  releabs  15349  absrdbnd  15369  rexuzre  15380  limsupgre  15508  lo1bddrp  15552  rlimclim1  15572  rlimresb  15592  rlimrege0  15606  o1add  15641  o1sub  15643  climsqz  15668  climsqz2  15669  rlimsqzlem  15676  rlimsqz  15677  rlimsqz2  15678  rlimno1  15681  isercoll  15695  caucvgrlem  15700  iseraltlem3  15711  o1fsum  15841  cvgcmp  15844  cvgcmpce  15846  climcnds  15881  expcnv  15894  cvgrat  15913  mertenslem2  15915  fprodle  16026  eftlub  16141  rpnnen2lem12  16257  bitsfzo  16469  isprm5  16742  isprm7  16743  eulerthlem2  16817  pcmpt2  16929  pcfac  16935  prmreclem3  16954  prmreclem4  16955  prmreclem5  16956  4sqlem11  16991  vdwlem1  17017  vdwlem3  17019  setsstruct2  17210  prdsxmetlem  24425  nrmmetd  24631  nm2dif  24682  nlmvscnlem2  24742  nmoco  24794  nmotri  24796  nghmcn  24802  icccmplem2  24881  reconnlem2  24885  elii1  24994  xrhmeo  25005  cnheiborlem  25013  bndth  25017  tcphcphlem1  25294  ipcnlem2  25303  cncmet  25381  trirn  25459  minveclem2  25485  minveclem4  25491  ivthlem2  25511  ovolunlem1a  25555  ovolunlem1  25556  ovolfiniun  25560  ovoliunlem1  25561  ovolicc2lem4  25579  ovolicc2lem5  25580  ovolicopnf  25583  nulmbl2  25595  ioombl1lem4  25620  ioorcl2  25631  uniioombllem3  25644  uniioombllem4  25645  uniioombllem5  25646  volcn  25665  vitalilem2  25668  vitali  25672  mbfi1fseqlem5  25778  mbfi1fseqlem6  25779  itg2splitlem  25807  itg2monolem1  25809  itg2monolem3  25811  itg2mono  25812  itg2cnlem1  25820  itgle  25869  bddmulibl  25898  bddiblnc  25901  ditgsplitlem  25919  dveflem  26038  dvlip  26052  dveq0  26059  dvfsumabs  26082  dvfsumlem1  26085  dvfsumlem2  26086  dvfsumlem3  26087  dvfsumlem4  26088  dvfsum2  26093  fta1glem2  26226  dgradd2  26325  plydiveu  26359  fta1lem  26368  aalioulem2  26394  aalioulem3  26395  aalioulem4  26396  aalioulem5  26397  aaliou3lem8  26406  aaliou3lem9  26411  ulmbdd  26458  ulmcn  26459  mtest  26464  mtestbdd  26465  abelthlem2  26492  abelthlem7  26498  pilem2  26512  tanabsge  26568  cosordlem  26592  tanord  26600  logneg2  26677  abslogle  26680  dvlog2lem  26714  cxple2a  26761  abscxpbnd  26815  atans2  26993  leibpi  27004  o1cxp  27036  cxploglim2  27040  jensenlem2  27049  emcllem6  27062  harmoniclbnd  27070  harmonicubnd  27071  harmonicbnd4  27072  fsumharmonic  27073  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem5  27094  lgambdd  27098  ftalem2  27135  basellem3  27144  basellem5  27146  basellem6  27147  dvdsflsumcom  27249  fsumfldivdiaglem  27250  ppiub  27265  chtublem  27272  logfac2  27278  chpub  27281  logfacubnd  27282  logfaclbnd  27283  logfacbnd3  27284  logexprlim  27286  bcmono  27338  bpos1lem  27343  bposlem1  27345  bposlem2  27346  bposlem3  27347  bposlem4  27348  bposlem5  27349  bposlem6  27350  bposlem7  27351  bposlem9  27353  lgsdirprm  27392  lgsquadlem1  27441  2lgslem1c  27454  2sqlem8  27487  chebbnd1lem1  27530  chebbnd1lem3  27532  chtppilimlem1  27534  chpchtlim  27540  vmadivsumb  27544  rplogsumlem1  27545  rplogsumlem2  27546  rpvmasumlem  27548  dchrisumlema  27549  dchrisumlem2  27551  dchrisumlem3  27552  dchrmusum2  27555  dchrvmasumlem2  27559  dchrvmasumlem3  27560  dchrvmasumlema  27561  dchrvmasumiflem1  27562  dchrisum0flblem1  27569  dchrisum0flblem2  27570  dchrisum0fno1  27572  dchrisum0re  27574  dchrisum0lem1b  27576  dchrisum0lem1  27577  dchrisum0lem2a  27578  dchrisum0  27581  rplogsum  27588  mudivsum  27591  mulogsumlem  27592  logdivsum  27594  mulog2sumlem1  27595  mulog2sumlem2  27596  2vmadivsumlem  27601  log2sumbnd  27605  selberglem2  27607  selbergb  27610  selberg2lem  27611  selberg2b  27613  chpdifbndlem1  27614  logdivbnd  27617  selberg3lem1  27618  selberg3lem2  27619  selberg4lem1  27621  pntrmax  27625  pntrsumo1  27626  pntrsumbnd  27627  pntrlog2bndlem1  27638  pntrlog2bndlem2  27639  pntrlog2bndlem3  27640  pntrlog2bndlem5  27642  pntrlog2bndlem6  27644  pntrlog2bnd  27645  pntpbnd1a  27646  pntpbnd1  27647  pntpbnd2  27648  pntibndlem2  27652  pntibndlem3  27653  pntlemg  27659  pntlemr  27663  pntlemj  27664  pntlemf  27666  pntlemk  27667  pntlemo  27668  pntleml  27672  abvcxp  27676  qabvle  27686  padicabv  27691  ostth2lem2  27695  ostth2lem3  27696  ostth3  27699  axlowdimlem16  29155  axcontlem8  29169  axcontlem10  29171  wwlksm1edg  30078  wwlksubclwwlk  30257  smcnlem  30897  nmoub3i  30973  ubthlem3  31072  minvecolem2  31075  minvecolem3  31076  minvecolem4  31080  htthlem  31117  bcs2  31382  pjhthlem1  31591  cnlnadjlem2  32268  cnlnadjlem7  32273  nmopadjlem  32289  nmoptrii  32294  nmopcoadji  32301  leopnmid  32338  cdj1i  32633  nndiffz1  32985  nexple  33032  oexpled  33035  pmtrto1cl  33276  psgnfzto1stlem  33277  fzto1st  33280  psgnfzto1st  33282  cyc3conja  33334  constrresqrtcl  34071  cos9thpiminplylem1  34076  smatrcl  34090  submateqlem1  34101  esumpcvgval  34372  oddpwdc  34648  eulerpartlems  34654  eulerpartlemgc  34656  eulerpartlemb  34662  dstfrvunirn  34769  orvclteinc  34770  ballotlemsima  34810  ballotlemfrcn0  34824  signstfveq0  34868  fsum2dsub  34898  breprexplemc  34923  breprexp  34924  logdivsqrle  34941  hgt750lemb  34947  hgt750leme  34949  tgoldbachgnn  34950  dnibndlem2  36914  dnibndlem6  36918  dnibndlem9  36921  dnibndlem10  36922  dnibndlem11  36923  dnibndlem12  36924  knoppcnlem4  36931  unblimceq0lem  36941  unblimceq0  36942  unbdqndv2lem2  36945  knoppndvlem11  36957  knoppndvlem14  36960  knoppndvlem15  36961  knoppndvlem18  36964  knoppndvlem21  36967  poimirlem6  38122  poimirlem7  38123  poimirlem13  38129  poimirlem15  38131  poimirlem29  38145  mblfinlem2  38154  mblfinlem3  38155  mblfinlem4  38156  ismblfin  38157  itg2addnc  38170  iblmulc2nc  38181  ftc1anclem7  38195  ftc1anclem8  38196  filbcmb  38236  geomcau  38255  prdsbnd  38289  cntotbnd  38292  bfplem2  38319  rrntotbnd  38332  iccbnd  38336  lcmineqlem20  42662  lcmineqlem21  42663  lcmineqlem22  42664  3lexlogpow5ineq2  42669  3lexlogpow5ineq5  42674  aks4d1p1p2  42684  aks4d1p1p4  42685  aks4d1p1p7  42688  aks4d1p1p5  42689  aks4d1p1  42690  aks4d1p2  42691  aks4d1p3  42692  aks4d1p5  42694  aks4d1p6  42695  aks4d1p7d1  42696  aks4d1p7  42697  aks4d1p8  42701  posbezout  42714  aks6d1c1  42730  aks6d1c2lem4  42741  2np3bcnp1  42758  sticksstones6  42765  sticksstones7  42766  sticksstones10  42769  sticksstones12a  42771  sticksstones12  42772  sticksstones22  42782  bcled  42792  bcle2d  42793  aks6d1c7lem1  42794  aks6d1c7lem2  42795  unitscyglem4  42812  lzunuz  43346  irrapxlem3  43398  irrapxlem4  43399  irrapxlem5  43400  pellexlem2  43404  pell1qrge1  43444  monotoddzzfi  43516  jm2.17a  43534  rmygeid  43538  fzmaxdif  43555  jm2.27c  43581  jm3.1lem1  43591  expdiophlem1  43595  fzunt  44028  fzuntd  44029  fzunt1d  44030  fzuntgd  44031  imo72b2lem0  44738  int-ineqtransd  44767  dvgrat  44885  monoords  45873  absnpncan2d  45878  absnpncan3d  45883  ssfiunibd  45885  rexabslelem  45989  uzublem  46001  sqrlearg  46126  fmul01  46153  fmul01lt1lem1  46157  fmul01lt1lem2  46158  climsuselem1  46180  climsuse  46181  limsupresico  46271  limsupubuzlem  46283  limsupmnfuzlem  46297  limsupre3uzlem  46306  liminfresico  46342  limsup10exlem  46343  cnrefiisplem  46400  dvdivbd  46494  dvbdfbdioolem2  46500  ioodvbdlimc1lem1  46502  ioodvbdlimc1lem2  46503  ioodvbdlimc2lem  46505  dvnmul  46514  dvnprodlem1  46517  dvnprodlem2  46518  iblspltprt  46544  itgspltprt  46550  stoweidlem1  46572  stoweidlem3  46574  stoweidlem5  46576  stoweidlem11  46582  stoweidlem17  46588  stoweidlem20  46591  stoweidlem26  46597  stoweidlem34  46605  wallispilem4  46639  stirlinglem11  46655  stirlinglem12  46656  stirlinglem13  46657  fourierdlem12  46690  fourierdlem15  46693  fourierdlem20  46698  fourierdlem30  46708  fourierdlem39  46717  fourierdlem42  46720  fourierdlem47  46724  fourierdlem50  46727  fourierdlem64  46741  fourierdlem65  46742  fourierdlem68  46745  fourierdlem73  46750  fourierdlem77  46754  fourierdlem79  46756  fourierdlem87  46764  elaa2lem  46804  etransclem23  46828  ioorrnopnlem  46875  salgencntex  46914  sge0le  46978  sge0isum  46998  sge0xaddlem1  47004  hoicvr  47119  hsphoidmvle2  47156  hoidmv1lelem1  47162  hoidmv1lelem2  47163  hoidmv1lelem3  47164  hoidmvlelem1  47166  hoidmvlelem2  47167  hoidmvlelem4  47169  hspmbllem1  47197  hspmbllem2  47198  smfmullem1  47362  smfmullem2  47363  smfmullem3  47364  smfsuplem1  47382  ormkglobd  47448  natglobalincr  47450  2ltceilhalf  47923  ceilhalfnn  47931  modmknepk  47959  lighneallem4a  48214  nprmdvdsfacm1lem4  48229  gpgusgralem  48675  gpgedgvtx1  48681  gpg3kgrtriexlem4  48705  gpg3kgrtriexlem6  48707  fllog2  49187  itcovalt2lem2lem1  49292