Theorem letrd 11418

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154   ≤ cle 11296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-pre-lttri 11229  ax-pre-lttrn 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301

This theorem is referenced by:  lesub3d  11881  supmul1  12237  supmul  12240  nn0negleid  12578  eluzuzle  12887  iccsplit  13525  supicc  13541  fzdisj  13591  ssfzunsnext  13609  difelfzle  13681  flwordi  13852  flleceil  13893  uzsup  13903  modltm1p1mod  13964  seqf1olem1  14082  zzlesq  14245  bernneq  14268  bernneq3  14270  discr1  14278  faclbnd  14329  faclbnd4lem1  14332  facubnd  14339  seqcoll  14503  01sqrexlem7  15287  absle  15354  releabs  15360  absrdbnd  15380  rexuzre  15391  limsupgre  15517  lo1bddrp  15561  rlimclim1  15581  rlimresb  15601  rlimrege0  15615  o1add  15650  o1sub  15652  climsqz  15677  climsqz2  15678  rlimsqzlem  15685  rlimsqz  15686  rlimsqz2  15687  rlimno1  15690  isercoll  15704  caucvgrlem  15709  iseraltlem3  15720  o1fsum  15849  cvgcmp  15852  cvgcmpce  15854  climcnds  15887  expcnv  15900  cvgrat  15919  mertenslem2  15921  fprodle  16032  eftlub  16145  rpnnen2lem12  16261  bitsfzo  16472  isprm5  16744  isprm7  16745  eulerthlem2  16819  pcmpt2  16931  pcfac  16937  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  4sqlem11  16993  vdwlem1  17019  vdwlem3  17021  setsstruct2  17211  prdsxmetlem  24378  nrmmetd  24587  nm2dif  24638  nlmvscnlem2  24706  nmoco  24758  nmotri  24760  nghmcn  24766  icccmplem2  24845  reconnlem2  24849  elii1  24964  xrhmeo  24977  cnheiborlem  24986  bndth  24990  tcphcphlem1  25269  ipcnlem2  25278  cncmet  25356  trirn  25434  minveclem2  25460  minveclem4  25466  ivthlem2  25487  ovolunlem1a  25531  ovolunlem1  25532  ovolfiniun  25536  ovoliunlem1  25537  ovolicc2lem4  25555  ovolicc2lem5  25556  ovolicopnf  25559  nulmbl2  25571  ioombl1lem4  25596  ioorcl2  25607  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  volcn  25641  vitalilem2  25644  vitali  25648  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  itg2splitlem  25783  itg2monolem1  25785  itg2monolem3  25787  itg2mono  25788  itg2cnlem1  25796  itgle  25845  bddmulibl  25874  bddiblnc  25877  ditgsplitlem  25895  dveflem  26017  dvlip  26032  dveq0  26039  dvfsumabs  26063  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsum2  26075  fta1glem2  26208  dgradd2  26308  plydiveu  26340  fta1lem  26349  aalioulem2  26375  aalioulem3  26376  aalioulem4  26377  aalioulem5  26378  aaliou3lem8  26387  aaliou3lem9  26392  ulmbdd  26441  ulmcn  26442  mtest  26447  mtestbdd  26448  abelthlem2  26476  abelthlem7  26482  pilem2  26496  tanabsge  26548  cosordlem  26572  tanord  26580  logneg2  26657  abslogle  26660  dvlog2lem  26694  cxple2a  26741  abscxpbnd  26796  atans2  26974  leibpi  26985  o1cxp  27018  cxploglim2  27022  jensenlem2  27031  emcllem6  27044  harmoniclbnd  27052  harmonicubnd  27053  harmonicbnd4  27054  fsumharmonic  27055  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem5  27076  lgambdd  27080  ftalem2  27117  basellem3  27126  basellem5  27128  basellem6  27129  dvdsflsumcom  27231  fsumfldivdiaglem  27232  ppiub  27248  chtublem  27255  logfac2  27261  chpub  27264  logfacubnd  27265  logfaclbnd  27266  logfacbnd3  27267  logexprlim  27269  bcmono  27321  bpos1lem  27326  bposlem1  27328  bposlem2  27329  bposlem3  27330  bposlem4  27331  bposlem5  27332  bposlem6  27333  bposlem7  27334  bposlem9  27336  lgsdirprm  27375  lgsquadlem1  27424  2lgslem1c  27437  2sqlem8  27470  chebbnd1lem1  27513  chebbnd1lem3  27515  chtppilimlem1  27517  chpchtlim  27523  vmadivsumb  27527  rplogsumlem1  27528  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlema  27532  dchrisumlem2  27534  dchrisumlem3  27535  dchrmusum2  27538  dchrvmasumlem2  27542  dchrvmasumlem3  27543  dchrvmasumlema  27544  dchrvmasumiflem1  27545  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0fno1  27555  dchrisum0re  27557  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0  27564  rplogsum  27571  mudivsum  27574  mulogsumlem  27575  logdivsum  27577  mulog2sumlem1  27578  mulog2sumlem2  27579  2vmadivsumlem  27584  log2sumbnd  27588  selberglem2  27590  selbergb  27593  selberg2lem  27594  selberg2b  27596  chpdifbndlem1  27597  logdivbnd  27600  selberg3lem1  27601  selberg3lem2  27602  selberg4lem1  27604  pntrmax  27608  pntrsumo1  27609  pntrsumbnd  27610  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntibndlem2  27635  pntibndlem3  27636  pntlemg  27642  pntlemr  27646  pntlemj  27647  pntlemf  27649  pntlemk  27650  pntlemo  27651  pntleml  27655  abvcxp  27659  qabvle  27669  padicabv  27674  ostth2lem2  27678  ostth2lem3  27679  ostth3  27682  axlowdimlem16  28972  axcontlem8  28986  axcontlem10  28988  wwlksm1edg  29901  wwlksubclwwlk  30077  smcnlem  30716  nmoub3i  30792  ubthlem3  30891  minvecolem2  30894  minvecolem3  30895  minvecolem4  30899  htthlem  30936  bcs2  31201  pjhthlem1  31410  cnlnadjlem2  32087  cnlnadjlem7  32092  nmopadjlem  32108  nmoptrii  32113  nmopcoadji  32120  leopnmid  32157  cdj1i  32452  nndiffz1  32788  nexple  32833  pmtrto1cl  33119  psgnfzto1stlem  33120  fzto1st  33123  psgnfzto1st  33125  cyc3conja  33177  smatrcl  33795  submateqlem1  33806  esumpcvgval  34079  oddpwdc  34356  eulerpartlems  34362  eulerpartlemgc  34364  eulerpartlemb  34370  dstfrvunirn  34477  orvclteinc  34478  ballotlemsima  34518  ballotlemfrcn0  34532  signstfveq0  34592  fsum2dsub  34622  breprexplemc  34647  breprexp  34648  logdivsqrle  34665  hgt750lemb  34671  hgt750leme  34673  tgoldbachgnn  34674  dnibndlem2  36480  dnibndlem6  36484  dnibndlem9  36487  dnibndlem10  36488  dnibndlem11  36489  dnibndlem12  36490  knoppcnlem4  36497  unblimceq0lem  36507  unblimceq0  36508  unbdqndv2lem2  36511  knoppndvlem11  36523  knoppndvlem14  36526  knoppndvlem15  36527  knoppndvlem18  36530  knoppndvlem21  36533  poimirlem6  37633  poimirlem7  37634  poimirlem13  37640  poimirlem15  37642  poimirlem29  37656  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnc  37681  iblmulc2nc  37692  ftc1anclem7  37706  ftc1anclem8  37707  filbcmb  37747  geomcau  37766  prdsbnd  37800  cntotbnd  37803  bfplem2  37830  rrntotbnd  37843  iccbnd  37847  lcmineqlem20  42049  lcmineqlem21  42050  lcmineqlem22  42051  3lexlogpow5ineq2  42056  3lexlogpow5ineq5  42061  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p2  42078  aks4d1p3  42079  aks4d1p5  42081  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8  42088  posbezout  42101  aks6d1c1  42117  aks6d1c2lem4  42128  2np3bcnp1  42145  sticksstones6  42152  sticksstones7  42153  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  sticksstones22  42169  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  aks6d1c7lem2  42182  unitscyglem4  42199  metakunt1  42206  metakunt12  42217  metakunt28  42233  lzunuz  42779  irrapxlem3  42835  irrapxlem4  42836  irrapxlem5  42837  pellexlem2  42841  pell1qrge1  42881  monotoddzzfi  42954  jm2.17a  42972  rmygeid  42976  fzmaxdif  42993  jm2.27c  43019  jm3.1lem1  43029  expdiophlem1  43033  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  imo72b2lem0  44178  int-ineqtransd  44207  dvgrat  44331  monoords  45309  absnpncan2d  45314  absnpncan3d  45319  ssfiunibd  45321  leadd12dd  45328  rexabslelem  45429  uzublem  45441  sqrlearg  45566  fmul01  45595  fmul01lt1lem1  45599  fmul01lt1lem2  45600  climsuselem1  45622  climsuse  45623  limsupresico  45715  limsupubuzlem  45727  limsupmnfuzlem  45741  limsupre3uzlem  45750  liminfresico  45786  limsup10exlem  45787  cnrefiisplem  45844  dvdivbd  45938  dvbdfbdioolem2  45944  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  iblspltprt  45988  itgspltprt  45994  stoweidlem1  46016  stoweidlem3  46018  stoweidlem5  46020  stoweidlem11  46026  stoweidlem17  46032  stoweidlem20  46035  stoweidlem26  46041  stoweidlem34  46049  wallispilem4  46083  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  fourierdlem12  46134  fourierdlem15  46137  fourierdlem20  46142  fourierdlem30  46152  fourierdlem39  46161  fourierdlem42  46164  fourierdlem47  46168  fourierdlem50  46171  fourierdlem64  46185  fourierdlem65  46186  fourierdlem68  46189  fourierdlem73  46194  fourierdlem77  46198  fourierdlem79  46200  fourierdlem87  46208  elaa2lem  46248  etransclem23  46272  ioorrnopnlem  46319  salgencntex  46358  sge0le  46422  sge0isum  46442  sge0xaddlem1  46448  hoicvr  46563  hsphoidmvle2  46600  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem4  46613  hspmbllem1  46641  hspmbllem2  46642  smfmullem1  46806  smfmullem2  46807  smfmullem3  46808  smfsuplem1  46826  ormkglobd  46890  natglobalincr  46892  lighneallem4a  47595  gpgusgralem  48011  2ltceilhalf  48015  gpgedgvtx1  48020  gpg3nbgrvtxlem  48023  gpg3kgrtriexlem4  48042  gpg3kgrtriexlem6  48044  fllog2  48489  itcovalt2lem2lem1  48594