Theorem letrd 11270

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   class class class wbr 5089  ℝcr 11005   ≤ cle 11147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-pre-lttri 11080  ax-pre-lttrn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152

This theorem is referenced by:  lesub3d  11735  le2addd  11736  supmul1  12091  supmul  12094  nn0negleid  12433  eluzuzle  12741  iccsplit  13385  supicc  13401  fzdisj  13451  ssfzunsnext  13469  difelfzle  13541  flwordi  13716  flleceil  13757  uzsup  13767  modltm1p1mod  13830  seqf1olem1  13948  zzlesq  14113  bernneq  14136  bernneq3  14138  discr1  14146  faclbnd  14197  faclbnd4lem1  14200  facubnd  14207  seqcoll  14371  01sqrexlem7  15155  absle  15223  releabs  15229  absrdbnd  15249  rexuzre  15260  limsupgre  15388  lo1bddrp  15432  rlimclim1  15452  rlimresb  15472  rlimrege0  15486  o1add  15521  o1sub  15523  climsqz  15548  climsqz2  15549  rlimsqzlem  15556  rlimsqz  15557  rlimsqz2  15558  rlimno1  15561  isercoll  15575  caucvgrlem  15580  iseraltlem3  15591  o1fsum  15720  cvgcmp  15723  cvgcmpce  15725  climcnds  15758  expcnv  15771  cvgrat  15790  mertenslem2  15792  fprodle  15903  eftlub  16018  rpnnen2lem12  16134  bitsfzo  16346  isprm5  16618  isprm7  16619  eulerthlem2  16693  pcmpt2  16805  pcfac  16811  prmreclem3  16830  prmreclem4  16831  prmreclem5  16832  4sqlem11  16867  vdwlem1  16893  vdwlem3  16895  setsstruct2  17085  prdsxmetlem  24283  nrmmetd  24489  nm2dif  24540  nlmvscnlem2  24600  nmoco  24652  nmotri  24654  nghmcn  24660  icccmplem2  24739  reconnlem2  24743  elii1  24858  xrhmeo  24871  cnheiborlem  24880  bndth  24884  tcphcphlem1  25162  ipcnlem2  25171  cncmet  25249  trirn  25327  minveclem2  25353  minveclem4  25359  ivthlem2  25380  ovolunlem1a  25424  ovolunlem1  25425  ovolfiniun  25429  ovoliunlem1  25430  ovolicc2lem4  25448  ovolicc2lem5  25449  ovolicopnf  25452  nulmbl2  25464  ioombl1lem4  25489  ioorcl2  25500  uniioombllem3  25513  uniioombllem4  25514  uniioombllem5  25515  volcn  25534  vitalilem2  25537  vitali  25541  mbfi1fseqlem5  25647  mbfi1fseqlem6  25648  itg2splitlem  25676  itg2monolem1  25678  itg2monolem3  25680  itg2mono  25681  itg2cnlem1  25689  itgle  25738  bddmulibl  25767  bddiblnc  25770  ditgsplitlem  25788  dveflem  25910  dvlip  25925  dveq0  25932  dvfsumabs  25956  dvfsumlem1  25959  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem3  25962  dvfsumlem4  25963  dvfsum2  25968  fta1glem2  26101  dgradd2  26201  plydiveu  26233  fta1lem  26242  aalioulem2  26268  aalioulem3  26269  aalioulem4  26270  aalioulem5  26271  aaliou3lem8  26280  aaliou3lem9  26285  ulmbdd  26334  ulmcn  26335  mtest  26340  mtestbdd  26341  abelthlem2  26369  abelthlem7  26375  pilem2  26389  tanabsge  26442  cosordlem  26466  tanord  26474  logneg2  26551  abslogle  26554  dvlog2lem  26588  cxple2a  26635  abscxpbnd  26690  atans2  26868  leibpi  26879  o1cxp  26912  cxploglim2  26916  jensenlem2  26925  emcllem6  26938  harmoniclbnd  26946  harmonicubnd  26947  harmonicbnd4  26948  fsumharmonic  26949  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamgulmlem5  26970  lgambdd  26974  ftalem2  27011  basellem3  27020  basellem5  27022  basellem6  27023  dvdsflsumcom  27125  fsumfldivdiaglem  27126  ppiub  27142  chtublem  27149  logfac2  27155  chpub  27158  logfacubnd  27159  logfaclbnd  27160  logfacbnd3  27161  logexprlim  27163  bcmono  27215  bpos1lem  27220  bposlem1  27222  bposlem2  27223  bposlem3  27224  bposlem4  27225  bposlem5  27226  bposlem6  27227  bposlem7  27228  bposlem9  27230  lgsdirprm  27269  lgsquadlem1  27318  2lgslem1c  27331  2sqlem8  27364  chebbnd1lem1  27407  chebbnd1lem3  27409  chtppilimlem1  27411  chpchtlim  27417  vmadivsumb  27421  rplogsumlem1  27422  rplogsumlem2  27423  rpvmasumlem  27425  dchrisumlema  27426  dchrisumlem2  27428  dchrisumlem3  27429  dchrmusum2  27432  dchrvmasumlem2  27436  dchrvmasumlem3  27437  dchrvmasumlema  27438  dchrvmasumiflem1  27439  dchrisum0flblem1  27446  dchrisum0flblem2  27447  dchrisum0fno1  27449  dchrisum0re  27451  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2a  27455  dchrisum0  27458  rplogsum  27465  mudivsum  27468  mulogsumlem  27469  logdivsum  27471  mulog2sumlem1  27472  mulog2sumlem2  27473  2vmadivsumlem  27478  log2sumbnd  27482  selberglem2  27484  selbergb  27487  selberg2lem  27488  selberg2b  27490  chpdifbndlem1  27491  logdivbnd  27494  selberg3lem1  27495  selberg3lem2  27496  selberg4lem1  27498  pntrmax  27502  pntrsumo1  27503  pntrsumbnd  27504  pntrlog2bndlem1  27515  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntrlog2bnd  27522  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntibndlem2  27529  pntibndlem3  27530  pntlemg  27536  pntlemr  27540  pntlemj  27541  pntlemf  27543  pntlemk  27544  pntlemo  27545  pntleml  27549  abvcxp  27553  qabvle  27563  padicabv  27568  ostth2lem2  27572  ostth2lem3  27573  ostth3  27576  axlowdimlem16  28935  axcontlem8  28949  axcontlem10  28951  wwlksm1edg  29859  wwlksubclwwlk  30038  smcnlem  30677  nmoub3i  30753  ubthlem3  30852  minvecolem2  30855  minvecolem3  30856  minvecolem4  30860  htthlem  30897  bcs2  31162  pjhthlem1  31371  cnlnadjlem2  32048  cnlnadjlem7  32053  nmopadjlem  32069  nmoptrii  32074  nmopcoadji  32081  leopnmid  32118  cdj1i  32413  nndiffz1  32769  nexple  32827  oexpled  32830  pmtrto1cl  33068  psgnfzto1stlem  33069  fzto1st  33072  psgnfzto1st  33074  cyc3conja  33126  constrresqrtcl  33790  cos9thpiminplylem1  33795  smatrcl  33809  submateqlem1  33820  esumpcvgval  34091  oddpwdc  34367  eulerpartlems  34373  eulerpartlemgc  34375  eulerpartlemb  34381  dstfrvunirn  34488  orvclteinc  34489  ballotlemsima  34529  ballotlemfrcn0  34543  signstfveq0  34590  fsum2dsub  34620  breprexplemc  34645  breprexp  34646  logdivsqrle  34663  hgt750lemb  34669  hgt750leme  34671  tgoldbachgnn  34672  dnibndlem2  36521  dnibndlem6  36525  dnibndlem9  36528  dnibndlem10  36529  dnibndlem11  36530  dnibndlem12  36531  knoppcnlem4  36538  unblimceq0lem  36548  unblimceq0  36549  unbdqndv2lem2  36552  knoppndvlem11  36564  knoppndvlem14  36567  knoppndvlem15  36568  knoppndvlem18  36571  knoppndvlem21  36574  poimirlem6  37674  poimirlem7  37675  poimirlem13  37681  poimirlem15  37683  poimirlem29  37697  mblfinlem2  37706  mblfinlem3  37707  mblfinlem4  37708  ismblfin  37709  itg2addnc  37722  iblmulc2nc  37733  ftc1anclem7  37747  ftc1anclem8  37748  filbcmb  37788  geomcau  37807  prdsbnd  37841  cntotbnd  37844  bfplem2  37871  rrntotbnd  37884  iccbnd  37888  lcmineqlem20  42089  lcmineqlem21  42090  lcmineqlem22  42091  3lexlogpow5ineq2  42096  3lexlogpow5ineq5  42101  aks4d1p1p2  42111  aks4d1p1p4  42112  aks4d1p1p7  42115  aks4d1p1p5  42116  aks4d1p1  42117  aks4d1p2  42118  aks4d1p3  42119  aks4d1p5  42121  aks4d1p6  42122  aks4d1p7d1  42123  aks4d1p7  42124  aks4d1p8  42128  posbezout  42141  aks6d1c1  42157  aks6d1c2lem4  42168  2np3bcnp1  42185  sticksstones6  42192  sticksstones7  42193  sticksstones10  42196  sticksstones12a  42198  sticksstones12  42199  sticksstones22  42209  bcled  42219  bcle2d  42220  aks6d1c7lem1  42221  aks6d1c7lem2  42222  unitscyglem4  42239  lzunuz  42809  irrapxlem3  42865  irrapxlem4  42866  irrapxlem5  42867  pellexlem2  42871  pell1qrge1  42911  monotoddzzfi  42983  jm2.17a  43001  rmygeid  43005  fzmaxdif  43022  jm2.27c  43048  jm3.1lem1  43058  expdiophlem1  43062  fzunt  43496  fzuntd  43497  fzunt1d  43498  fzuntgd  43499  imo72b2lem0  44206  int-ineqtransd  44235  dvgrat  44353  monoords  45346  absnpncan2d  45351  absnpncan3d  45356  ssfiunibd  45358  rexabslelem  45464  uzublem  45476  sqrlearg  45601  fmul01  45628  fmul01lt1lem1  45632  fmul01lt1lem2  45633  climsuselem1  45655  climsuse  45656  limsupresico  45746  limsupubuzlem  45758  limsupmnfuzlem  45772  limsupre3uzlem  45781  liminfresico  45817  limsup10exlem  45818  cnrefiisplem  45875  dvdivbd  45969  dvbdfbdioolem2  45975  ioodvbdlimc1lem1  45977  ioodvbdlimc1lem2  45978  ioodvbdlimc2lem  45980  dvnmul  45989  dvnprodlem1  45992  dvnprodlem2  45993  iblspltprt  46019  itgspltprt  46025  stoweidlem1  46047  stoweidlem3  46049  stoweidlem5  46051  stoweidlem11  46057  stoweidlem17  46063  stoweidlem20  46066  stoweidlem26  46072  stoweidlem34  46080  wallispilem4  46114  stirlinglem11  46130  stirlinglem12  46131  stirlinglem13  46132  fourierdlem12  46165  fourierdlem15  46168  fourierdlem20  46173  fourierdlem30  46183  fourierdlem39  46192  fourierdlem42  46195  fourierdlem47  46199  fourierdlem50  46202  fourierdlem64  46216  fourierdlem65  46217  fourierdlem68  46220  fourierdlem73  46225  fourierdlem77  46229  fourierdlem79  46231  fourierdlem87  46239  elaa2lem  46279  etransclem23  46303  ioorrnopnlem  46350  salgencntex  46389  sge0le  46453  sge0isum  46473  sge0xaddlem1  46479  hoicvr  46594  hsphoidmvle2  46631  hoidmv1lelem1  46637  hoidmv1lelem2  46638  hoidmv1lelem3  46639  hoidmvlelem1  46641  hoidmvlelem2  46642  hoidmvlelem4  46644  hspmbllem1  46672  hspmbllem2  46673  smfmullem1  46837  smfmullem2  46838  smfmullem3  46839  smfsuplem1  46857  ormkglobd  46921  natglobalincr  46923  2ltceilhalf  47367  ceilhalfnn  47375  modmknepk  47401  lighneallem4a  47647  gpgusgralem  48095  gpgedgvtx1  48101  gpg3kgrtriexlem4  48125  gpg3kgrtriexlem6  48127  fllog2  48608  itcovalt2lem2lem1  48713