Theorem letrd 11382

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   class class class wbr 5111  ℝcr 11114   ≤ cle 11259

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11172  ax-pre-lttri 11189  ax-pre-lttrn 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264

This theorem is used by:  lesub3d  11847  le2addd  11848  supmul1  12199  supmul  12202  nn0negleid  12571  eluzuzle  12887  iccsplit  13528  supicc  13544  fzdisj  13596  ssfzunsnext  13614  difelfzle  13686  flwordi  13863  flleceil  13904  uzsup  13914  modltm1p1mod  13977  seqf1olem1  14095  zzlesq  14260  bernneq  14283  bernneq3  14285  discr1  14293  faclbnd  14344  faclbnd4lem1  14347  facubnd  14354  seqcoll  14519  01sqrexlem7  15323  absle  15391  releabs  15397  absrdbnd  15417  rexuzre  15428  limsupgre  15556  lo1bddrp  15600  rlimclim1  15620  rlimresb  15640  rlimrege0  15654  o1add  15689  o1sub  15691  climsqz  15716  climsqz2  15717  rlimsqzlem  15724  rlimsqz  15725  rlimsqz2  15726  rlimno1  15729  isercoll  15743  caucvgrlem  15748  iseraltlem3  15759  o1fsum  15888  cvgcmp  15891  cvgcmpce  15893  climcnds  15928  expcnv  15941  cvgrat  15960  mertenslem2  15962  fprodle  16073  eftlub  16187  rpnnen2lem12  16303  bitsfzo  16515  isprm5  16788  isprm7  16789  eulerthlem2  16863  pcmpt2  16975  pcfac  16981  prmreclem3  17000  prmreclem4  17001  prmreclem5  17002  4sqlem11  17037  vdwlem1  17063  vdwlem3  17065  setsstruct2  17256  prdsxmetlem  24576  nrmmetd  24782  nm2dif  24833  nlmvscnlem2  24893  nmoco  24945  nmotri  24947  nghmcn  24953  icccmplem2  25032  reconnlem2  25036  elii1  25145  xrhmeo  25156  cnheiborlem  25164  bndth  25168  tcphcphlem1  25445  ipcnlem2  25454  cncmet  25532  trirn  25610  minveclem2  25636  minveclem4  25642  ivthlem2  25662  ovolunlem1a  25706  ovolunlem1  25707  ovolfiniun  25711  ovoliunlem1  25712  ovolicc2lem4  25730  ovolicc2lem5  25731  ovolicopnf  25734  nulmbl2  25746  ioombl1lem4  25771  ioorcl2  25782  uniioombllem3  25795  uniioombllem4  25796  uniioombllem5  25797  volcn  25816  vitalilem2  25819  vitali  25823  mbfi1fseqlem5  25929  mbfi1fseqlem6  25930  itg2splitlem  25958  itg2monolem1  25960  itg2monolem3  25962  itg2mono  25963  itg2cnlem1  25971  itgle  26020  bddmulibl  26049  bddiblnc  26052  ditgsplitlem  26070  dveflem  26189  dvlip  26203  dveq0  26210  dvfsumabs  26233  dvfsumlem1  26236  dvfsumlem2  26237  dvfsumlem3  26238  dvfsumlem4  26239  dvfsum2  26244  fta1glem2  26377  dgradd2  26476  plydiveu  26510  fta1lem  26519  aalioulem2  26547  aalioulem3  26548  aalioulem4  26549  aalioulem5  26550  aaliou3lem8  26559  aaliou3lem9  26564  ulmbdd  26612  ulmcn  26613  mtest  26618  mtestbdd  26619  abelthlem2  26646  abelthlem7  26652  pilem2  26666  tanabsge  26722  cosordlem  26746  tanord  26754  logneg2  26831  abslogle  26834  dvlog2lem  26868  cxple2a  26915  abscxpbnd  26969  atans2  27147  leibpi  27158  o1cxp  27190  cxploglim2  27194  jensenlem2  27203  emcllem6  27216  harmoniclbnd  27224  harmonicubnd  27225  harmonicbnd4  27226  fsumharmonic  27227  lgamgulmlem2  27245  lgamgulmlem3  27246  lgamgulmlem5  27248  lgambdd  27252  ftalem2  27289  basellem3  27298  basellem5  27300  basellem6  27301  dvdsflsumcom  27403  fsumfldivdiaglem  27404  ppiub  27419  chtublem  27426  logfac2  27432  chpub  27435  logfacubnd  27436  logfaclbnd  27437  logfacbnd3  27438  logexprlim  27440  bcmono  27492  bpos1lem  27497  bposlem1  27499  bposlem2  27500  bposlem3  27501  bposlem4  27502  bposlem5  27503  bposlem6  27504  bposlem7  27505  bposlem9  27507  lgsdirprm  27546  lgsquadlem1  27595  2lgslem1c  27608  2sqlem8  27641  chebbnd1lem1  27684  chebbnd1lem3  27686  chtppilimlem1  27688  chpchtlim  27694  vmadivsumb  27698  rplogsumlem1  27699  rplogsumlem2  27700  rpvmasumlem  27702  dchrisumlema  27703  dchrisumlem2  27705  dchrisumlem3  27706  dchrmusum2  27709  dchrvmasumlem2  27713  dchrvmasumlem3  27714  dchrvmasumlema  27715  dchrvmasumiflem1  27716  dchrisum0flblem1  27723  dchrisum0flblem2  27724  dchrisum0fno1  27726  dchrisum0re  27728  dchrisum0lem1b  27730  dchrisum0lem1  27731  dchrisum0lem2a  27732  dchrisum0  27735  rplogsum  27742  mudivsum  27745  mulogsumlem  27746  logdivsum  27748  mulog2sumlem1  27749  mulog2sumlem2  27750  2vmadivsumlem  27755  log2sumbnd  27759  selberglem2  27761  selbergb  27764  selberg2lem  27765  selberg2b  27767  chpdifbndlem1  27768  logdivbnd  27771  selberg3lem1  27772  selberg3lem2  27773  selberg4lem1  27775  pntrmax  27779  pntrsumo1  27780  pntrsumbnd  27781  pntrlog2bndlem1  27792  pntrlog2bndlem2  27793  pntrlog2bndlem3  27794  pntrlog2bndlem5  27796  pntrlog2bndlem6  27798  pntrlog2bnd  27799  pntpbnd1a  27800  pntpbnd1  27801  pntpbnd2  27802  pntibndlem2  27806  pntibndlem3  27807  pntlemg  27813  pntlemr  27817  pntlemj  27818  pntlemf  27820  pntlemk  27821  pntlemo  27822  pntleml  27826  abvcxp  27830  qabvle  27840  padicabv  27845  ostth2lem2  27849  ostth2lem3  27850  ostth3  27853  axlowdimlem16  29362  axcontlem8  29376  axcontlem10  29378  wwlksm1edg  30297  wwlksubclwwlk  30476  smcnlem  31120  nmoub3i  31196  ubthlem3  31295  minvecolem2  31298  minvecolem3  31299  minvecolem4  31303  htthlem  31340  bcs2  31605  pjhthlem1  31814  cnlnadjlem2  32491  cnlnadjlem7  32496  nmopadjlem  32512  nmoptrii  32517  nmopcoadji  32524  leopnmid  32561  cdj1i  32856  nndiffz1  33201  nexple  33247  oexpled  33250  pmtrto1cl  33483  psgnfzto1stlem  33484  fzto1st  33487  psgnfzto1st  33489  cyc3conja  33541  constrresqrtcl  34231  cos9thpiminplylem1  34236  smatrcl  34250  submateqlem1  34261  esumpcvgval  34532  oddpwdc  34809  eulerpartlems  34815  eulerpartlemgc  34817  eulerpartlemb  34823  dstfrvunirn  34930  orvclteinc  34931  ballotlemsima  34971  ballotlemfrcn0  34985  signstfveq0  35029  fsum2dsub  35059  breprexplemc  35084  breprexp  35085  logdivsqrle  35102  hgt750lemb  35108  hgt750leme  35110  tgoldbachgnn  35111  dnibndlem2  37125  dnibndlem6  37129  dnibndlem9  37132  dnibndlem10  37133  dnibndlem11  37134  dnibndlem12  37135  knoppcnlem4  37142  unblimceq0lem  37152  unblimceq0  37153  unbdqndv2lem2  37156  knoppndvlem11  37168  knoppndvlem14  37171  knoppndvlem15  37172  knoppndvlem18  37175  knoppndvlem21  37178  poimirlem6  38334  poimirlem7  38335  poimirlem13  38341  poimirlem15  38343  poimirlem29  38357  mblfinlem2  38366  mblfinlem3  38367  mblfinlem4  38368  ismblfin  38369  itg2addnc  38382  iblmulc2nc  38393  ftc1anclem7  38407  ftc1anclem8  38408  filbcmb  38449  geomcau  38468  prdsbnd  38502  cntotbnd  38505  bfplem2  38532  rrntotbnd  38545  iccbnd  38549  lcmineqlem20  42873  lcmineqlem21  42874  lcmineqlem22  42875  3lexlogpow5ineq2  42880  3lexlogpow5ineq5  42885  aks4d1p1p2  42895  aks4d1p1p4  42896  aks4d1p1p7  42899  aks4d1p1p5  42900  aks4d1p1  42901  aks4d1p2  42902  aks4d1p3  42903  aks4d1p5  42905  aks4d1p6  42906  aks4d1p7d1  42907  aks4d1p7  42908  aks4d1p8  42912  posbezout  42925  aks6d1c1  42941  aks6d1c2lem4  42952  2np3bcnp1  42969  sticksstones6  42976  sticksstones7  42977  sticksstones10  42980  sticksstones12a  42982  sticksstones12  42983  sticksstones22  42993  bcled  43003  bcle2d  43004  aks6d1c7lem1  43005  aks6d1c7lem2  43006  unitscyglem4  43023  lzunuz  43557  irrapxlem3  43609  irrapxlem4  43610  irrapxlem5  43611  pellexlem2  43615  pell1qrge1  43655  monotoddzzfi  43727  jm2.17a  43745  rmygeid  43749  fzmaxdif  43766  jm2.27c  43792  jm3.1lem1  43802  expdiophlem1  43806  fzunt  44239  fzuntd  44240  fzunt1d  44241  fzuntgd  44242  imo72b2lem0  44949  int-ineqtransd  44978  dvgrat  45080  monoords  46074  absnpncan2d  46079  absnpncan3d  46084  ssfiunibd  46086  rexabslelem  46190  uzublem  46202  sqrlearg  46327  fmul01  46354  fmul01lt1lem1  46358  fmul01lt1lem2  46359  climsuselem1  46381  climsuse  46382  limsupresico  46472  limsupubuzlem  46484  limsupmnfuzlem  46498  limsupre3uzlem  46507  liminfresico  46543  limsup10exlem  46544  cnrefiisplem  46601  dvdivbd  46695  dvbdfbdioolem2  46701  ioodvbdlimc1lem1  46703  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  dvnmul  46715  dvnprodlem1  46718  dvnprodlem2  46719  iblspltprt  46745  itgspltprt  46751  stoweidlem1  46773  stoweidlem3  46775  stoweidlem5  46777  stoweidlem11  46783  stoweidlem17  46789  stoweidlem20  46792  stoweidlem26  46798  stoweidlem34  46806  wallispilem4  46840  stirlinglem11  46856  stirlinglem12  46857  stirlinglem13  46858  fourierdlem12  46891  fourierdlem15  46894  fourierdlem20  46899  fourierdlem30  46909  fourierdlem39  46918  fourierdlem42  46921  fourierdlem47  46925  fourierdlem50  46928  fourierdlem64  46942  fourierdlem65  46943  fourierdlem68  46946  fourierdlem73  46951  fourierdlem77  46955  fourierdlem79  46957  fourierdlem87  46965  elaa2lem  47005  etransclem23  47029  ioorrnopnlem  47076  salgencntex  47115  sge0le  47179  sge0isum  47199  sge0xaddlem1  47205  hoicvr  47320  hsphoidmvle2  47357  hoidmv1lelem1  47363  hoidmv1lelem2  47364  hoidmv1lelem3  47365  hoidmvlelem1  47367  hoidmvlelem2  47368  hoidmvlelem4  47370  hspmbllem1  47398  hspmbllem2  47399  smfmullem1  47563  smfmullem2  47564  smfmullem3  47565  smfsuplem1  47583  ormkglobd  47649  natglobalincr  47651  2ltceilhalf  48127  ceilhalfnn  48135  modmknepk  48163  lighneallem4a  48418  nprmdvdsfacm1lem4  48433  gpgusgralem  48879  gpgedgvtx1  48885  gpg3kgrtriexlem4  48909  gpg3kgrtriexlem6  48911  fllog2  49405  itcovalt2lem2lem1  49510