Theorem letrd 11377

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 11314	. . 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 5112  ℝcr 11109   ≤ cle 11254

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 2738  ax-sep 5260  ax-nul 5272  ax-pow 5339  ax-pr 5407  ax-un 7738  ax-resscn 11167  ax-pre-lttri 11184  ax-pre-lttrn 11185

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-br 5113  df-opab 5177  df-mpt 5196  df-id 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  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 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259

This theorem is used by:  lesub3d  11842  le2addd  11843  supmul1  12194  supmul  12197  nn0negleid  12566  eluzuzle  12881  iccsplit  13522  supicc  13538  fzdisj  13590  ssfzunsnext  13608  difelfzle  13680  flwordi  13856  flleceil  13897  uzsup  13907  modltm1p1mod  13970  seqf1olem1  14088  zzlesq  14253  bernneq  14276  bernneq3  14278  discr1  14286  faclbnd  14337  faclbnd4lem1  14340  facubnd  14347  seqcoll  14512  01sqrexlem7  15310  absle  15378  releabs  15384  absrdbnd  15404  rexuzre  15415  limsupgre  15543  lo1bddrp  15587  rlimclim1  15607  rlimresb  15627  rlimrege0  15641  o1add  15676  o1sub  15678  climsqz  15703  climsqz2  15704  rlimsqzlem  15711  rlimsqz  15712  rlimsqz2  15713  rlimno1  15716  isercoll  15730  caucvgrlem  15735  iseraltlem3  15746  o1fsum  15876  cvgcmp  15879  cvgcmpce  15881  climcnds  15916  expcnv  15929  cvgrat  15948  mertenslem2  15950  fprodle  16061  eftlub  16175  rpnnen2lem12  16291  bitsfzo  16503  isprm5  16776  isprm7  16777  eulerthlem2  16851  pcmpt2  16963  pcfac  16969  prmreclem3  16988  prmreclem4  16989  prmreclem5  16990  4sqlem11  17025  vdwlem1  17051  vdwlem3  17053  setsstruct2  17244  prdsxmetlem  24540  nrmmetd  24746  nm2dif  24797  nlmvscnlem2  24857  nmoco  24909  nmotri  24911  nghmcn  24917  icccmplem2  24996  reconnlem2  25000  elii1  25109  xrhmeo  25120  cnheiborlem  25128  bndth  25132  tcphcphlem1  25409  ipcnlem2  25418  cncmet  25496  trirn  25574  minveclem2  25600  minveclem4  25606  ivthlem2  25626  ovolunlem1a  25670  ovolunlem1  25671  ovolfiniun  25675  ovoliunlem1  25676  ovolicc2lem4  25694  ovolicc2lem5  25695  ovolicopnf  25698  nulmbl2  25710  ioombl1lem4  25735  ioorcl2  25746  uniioombllem3  25759  uniioombllem4  25760  uniioombllem5  25761  volcn  25780  vitalilem2  25783  vitali  25787  mbfi1fseqlem5  25893  mbfi1fseqlem6  25894  itg2splitlem  25922  itg2monolem1  25924  itg2monolem3  25926  itg2mono  25927  itg2cnlem1  25935  itgle  25984  bddmulibl  26013  bddiblnc  26016  ditgsplitlem  26034  dveflem  26153  dvlip  26167  dveq0  26174  dvfsumabs  26197  dvfsumlem1  26200  dvfsumlem2  26201  dvfsumlem3  26202  dvfsumlem4  26203  dvfsum2  26208  fta1glem2  26341  dgradd2  26440  plydiveu  26474  fta1lem  26483  aalioulem2  26511  aalioulem3  26512  aalioulem4  26513  aalioulem5  26514  aaliou3lem8  26523  aaliou3lem9  26528  ulmbdd  26576  ulmcn  26577  mtest  26582  mtestbdd  26583  abelthlem2  26610  abelthlem7  26616  pilem2  26630  tanabsge  26686  cosordlem  26710  tanord  26718  logneg2  26795  abslogle  26798  dvlog2lem  26832  cxple2a  26879  abscxpbnd  26933  atans2  27111  leibpi  27122  o1cxp  27154  cxploglim2  27158  jensenlem2  27167  emcllem6  27180  harmoniclbnd  27188  harmonicubnd  27189  harmonicbnd4  27190  fsumharmonic  27191  lgamgulmlem2  27209  lgamgulmlem3  27210  lgamgulmlem5  27212  lgambdd  27216  ftalem2  27253  basellem3  27262  basellem5  27264  basellem6  27265  dvdsflsumcom  27367  fsumfldivdiaglem  27368  ppiub  27383  chtublem  27390  logfac2  27396  chpub  27399  logfacubnd  27400  logfaclbnd  27401  logfacbnd3  27402  logexprlim  27404  bcmono  27456  bpos1lem  27461  bposlem1  27463  bposlem2  27464  bposlem3  27465  bposlem4  27466  bposlem5  27467  bposlem6  27468  bposlem7  27469  bposlem9  27471  lgsdirprm  27510  lgsquadlem1  27559  2lgslem1c  27572  2sqlem8  27605  chebbnd1lem1  27648  chebbnd1lem3  27650  chtppilimlem1  27652  chpchtlim  27658  vmadivsumb  27662  rplogsumlem1  27663  rplogsumlem2  27664  rpvmasumlem  27666  dchrisumlema  27667  dchrisumlem2  27669  dchrisumlem3  27670  dchrmusum2  27673  dchrvmasumlem2  27677  dchrvmasumlem3  27678  dchrvmasumlema  27679  dchrvmasumiflem1  27680  dchrisum0flblem1  27687  dchrisum0flblem2  27688  dchrisum0fno1  27690  dchrisum0re  27692  dchrisum0lem1b  27694  dchrisum0lem1  27695  dchrisum0lem2a  27696  dchrisum0  27699  rplogsum  27706  mudivsum  27709  mulogsumlem  27710  logdivsum  27712  mulog2sumlem1  27713  mulog2sumlem2  27714  2vmadivsumlem  27719  log2sumbnd  27723  selberglem2  27725  selbergb  27728  selberg2lem  27729  selberg2b  27731  chpdifbndlem1  27732  logdivbnd  27735  selberg3lem1  27736  selberg3lem2  27737  selberg4lem1  27739  pntrmax  27743  pntrsumo1  27744  pntrsumbnd  27745  pntrlog2bndlem1  27756  pntrlog2bndlem2  27757  pntrlog2bndlem3  27758  pntrlog2bndlem5  27760  pntrlog2bndlem6  27762  pntrlog2bnd  27763  pntpbnd1a  27764  pntpbnd1  27765  pntpbnd2  27766  pntibndlem2  27770  pntibndlem3  27771  pntlemg  27777  pntlemr  27781  pntlemj  27782  pntlemf  27784  pntlemk  27785  pntlemo  27786  pntleml  27790  abvcxp  27794  qabvle  27804  padicabv  27809  ostth2lem2  27813  ostth2lem3  27814  ostth3  27817  axlowdimlem16  29322  axcontlem8  29336  axcontlem10  29338  wwlksm1edg  30245  wwlksubclwwlk  30424  smcnlem  31064  nmoub3i  31140  ubthlem3  31239  minvecolem2  31242  minvecolem3  31243  minvecolem4  31247  htthlem  31284  bcs2  31549  pjhthlem1  31758  cnlnadjlem2  32435  cnlnadjlem7  32440  nmopadjlem  32456  nmoptrii  32461  nmopcoadji  32468  leopnmid  32505  cdj1i  32800  nndiffz1  33146  nexple  33192  oexpled  33195  pmtrto1cl  33432  psgnfzto1stlem  33433  fzto1st  33436  psgnfzto1st  33438  cyc3conja  33490  constrresqrtcl  34180  cos9thpiminplylem1  34185  smatrcl  34199  submateqlem1  34210  esumpcvgval  34481  oddpwdc  34757  eulerpartlems  34763  eulerpartlemgc  34765  eulerpartlemb  34771  dstfrvunirn  34878  orvclteinc  34879  ballotlemsima  34919  ballotlemfrcn0  34933  signstfveq0  34977  fsum2dsub  35007  breprexplemc  35032  breprexp  35033  logdivsqrle  35050  hgt750lemb  35056  hgt750leme  35058  tgoldbachgnn  35059  dnibndlem2  37100  dnibndlem6  37104  dnibndlem9  37107  dnibndlem10  37108  dnibndlem11  37109  dnibndlem12  37110  knoppcnlem4  37117  unblimceq0lem  37127  unblimceq0  37128  unbdqndv2lem2  37131  knoppndvlem11  37143  knoppndvlem14  37146  knoppndvlem15  37147  knoppndvlem18  37150  knoppndvlem21  37153  poimirlem6  38309  poimirlem7  38310  poimirlem13  38316  poimirlem15  38318  poimirlem29  38332  mblfinlem2  38341  mblfinlem3  38342  mblfinlem4  38343  ismblfin  38344  itg2addnc  38357  iblmulc2nc  38368  ftc1anclem7  38382  ftc1anclem8  38383  filbcmb  38423  geomcau  38442  prdsbnd  38476  cntotbnd  38479  bfplem2  38506  rrntotbnd  38519  iccbnd  38523  lcmineqlem20  42847  lcmineqlem21  42848  lcmineqlem22  42849  3lexlogpow5ineq2  42854  3lexlogpow5ineq5  42859  aks4d1p1p2  42869  aks4d1p1p4  42870  aks4d1p1p7  42873  aks4d1p1p5  42874  aks4d1p1  42875  aks4d1p2  42876  aks4d1p3  42877  aks4d1p5  42879  aks4d1p6  42880  aks4d1p7d1  42881  aks4d1p7  42882  aks4d1p8  42886  posbezout  42899  aks6d1c1  42915  aks6d1c2lem4  42926  2np3bcnp1  42943  sticksstones6  42950  sticksstones7  42951  sticksstones10  42954  sticksstones12a  42956  sticksstones12  42957  sticksstones22  42967  bcled  42977  bcle2d  42978  aks6d1c7lem1  42979  aks6d1c7lem2  42980  unitscyglem4  42997  lzunuz  43531  irrapxlem3  43583  irrapxlem4  43584  irrapxlem5  43585  pellexlem2  43589  pell1qrge1  43629  monotoddzzfi  43701  jm2.17a  43719  rmygeid  43723  fzmaxdif  43740  jm2.27c  43766  jm3.1lem1  43776  expdiophlem1  43780  fzunt  44213  fzuntd  44214  fzunt1d  44215  fzuntgd  44216  imo72b2lem0  44923  int-ineqtransd  44952  dvgrat  45054  monoords  46048  absnpncan2d  46053  absnpncan3d  46058  ssfiunibd  46060  rexabslelem  46164  uzublem  46176  sqrlearg  46301  fmul01  46328  fmul01lt1lem1  46332  fmul01lt1lem2  46333  climsuselem1  46355  climsuse  46356  limsupresico  46446  limsupubuzlem  46458  limsupmnfuzlem  46472  limsupre3uzlem  46481  liminfresico  46517  limsup10exlem  46518  cnrefiisplem  46575  dvdivbd  46669  dvbdfbdioolem2  46675  ioodvbdlimc1lem1  46677  ioodvbdlimc1lem2  46678  ioodvbdlimc2lem  46680  dvnmul  46689  dvnprodlem1  46692  dvnprodlem2  46693  iblspltprt  46719  itgspltprt  46725  stoweidlem1  46747  stoweidlem3  46749  stoweidlem5  46751  stoweidlem11  46757  stoweidlem17  46763  stoweidlem20  46766  stoweidlem26  46772  stoweidlem34  46780  wallispilem4  46814  stirlinglem11  46830  stirlinglem12  46831  stirlinglem13  46832  fourierdlem12  46865  fourierdlem15  46868  fourierdlem20  46873  fourierdlem30  46883  fourierdlem39  46892  fourierdlem42  46895  fourierdlem47  46899  fourierdlem50  46902  fourierdlem64  46916  fourierdlem65  46917  fourierdlem68  46920  fourierdlem73  46925  fourierdlem77  46929  fourierdlem79  46931  fourierdlem87  46939  elaa2lem  46979  etransclem23  47003  ioorrnopnlem  47050  salgencntex  47089  sge0le  47153  sge0isum  47173  sge0xaddlem1  47179  hoicvr  47294  hsphoidmvle2  47331  hoidmv1lelem1  47337  hoidmv1lelem2  47338  hoidmv1lelem3  47339  hoidmvlelem1  47341  hoidmvlelem2  47342  hoidmvlelem4  47344  hspmbllem1  47372  hspmbllem2  47373  smfmullem1  47537  smfmullem2  47538  smfmullem3  47539  smfsuplem1  47557  ormkglobd  47623  natglobalincr  47625  2ltceilhalf  48101  ceilhalfnn  48109  modmknepk  48137  lighneallem4a  48392  nprmdvdsfacm1lem4  48407  gpgusgralem  48853  gpgedgvtx1  48859  gpg3kgrtriexlem4  48883  gpg3kgrtriexlem6  48885  fllog2  49380  itcovalt2lem2lem1  49485