Theorem letrd 11290

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   ≤ cle 11167

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-pre-lttri 11100  ax-pre-lttrn 11101

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172

This theorem is referenced by:  lesub3d  11755  le2addd  11756  supmul1  12111  supmul  12114  nn0negleid  12453  eluzuzle  12760  iccsplit  13401  supicc  13417  fzdisj  13467  ssfzunsnext  13485  difelfzle  13557  flwordi  13732  flleceil  13773  uzsup  13783  modltm1p1mod  13846  seqf1olem1  13964  zzlesq  14129  bernneq  14152  bernneq3  14154  discr1  14162  faclbnd  14213  faclbnd4lem1  14216  facubnd  14223  seqcoll  14387  01sqrexlem7  15171  absle  15239  releabs  15245  absrdbnd  15265  rexuzre  15276  limsupgre  15404  lo1bddrp  15448  rlimclim1  15468  rlimresb  15488  rlimrege0  15502  o1add  15537  o1sub  15539  climsqz  15564  climsqz2  15565  rlimsqzlem  15572  rlimsqz  15573  rlimsqz2  15574  rlimno1  15577  isercoll  15591  caucvgrlem  15596  iseraltlem3  15607  o1fsum  15736  cvgcmp  15739  cvgcmpce  15741  climcnds  15774  expcnv  15787  cvgrat  15806  mertenslem2  15808  fprodle  15919  eftlub  16034  rpnnen2lem12  16150  bitsfzo  16362  isprm5  16634  isprm7  16635  eulerthlem2  16709  pcmpt2  16821  pcfac  16827  prmreclem3  16846  prmreclem4  16847  prmreclem5  16848  4sqlem11  16883  vdwlem1  16909  vdwlem3  16911  setsstruct2  17101  prdsxmetlem  24312  nrmmetd  24518  nm2dif  24569  nlmvscnlem2  24629  nmoco  24681  nmotri  24683  nghmcn  24689  icccmplem2  24768  reconnlem2  24772  elii1  24887  xrhmeo  24900  cnheiborlem  24909  bndth  24913  tcphcphlem1  25191  ipcnlem2  25200  cncmet  25278  trirn  25356  minveclem2  25382  minveclem4  25388  ivthlem2  25409  ovolunlem1a  25453  ovolunlem1  25454  ovolfiniun  25458  ovoliunlem1  25459  ovolicc2lem4  25477  ovolicc2lem5  25478  ovolicopnf  25481  nulmbl2  25493  ioombl1lem4  25518  ioorcl2  25529  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  volcn  25563  vitalilem2  25566  vitali  25570  mbfi1fseqlem5  25676  mbfi1fseqlem6  25677  itg2splitlem  25705  itg2monolem1  25707  itg2monolem3  25709  itg2mono  25710  itg2cnlem1  25718  itgle  25767  bddmulibl  25796  bddiblnc  25799  ditgsplitlem  25817  dveflem  25939  dvlip  25954  dveq0  25961  dvfsumabs  25985  dvfsumlem1  25988  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem3  25991  dvfsumlem4  25992  dvfsum2  25997  fta1glem2  26130  dgradd2  26230  plydiveu  26262  fta1lem  26271  aalioulem2  26297  aalioulem3  26298  aalioulem4  26299  aalioulem5  26300  aaliou3lem8  26309  aaliou3lem9  26314  ulmbdd  26363  ulmcn  26364  mtest  26369  mtestbdd  26370  abelthlem2  26398  abelthlem7  26404  pilem2  26418  tanabsge  26471  cosordlem  26495  tanord  26503  logneg2  26580  abslogle  26583  dvlog2lem  26617  cxple2a  26664  abscxpbnd  26719  atans2  26897  leibpi  26908  o1cxp  26941  cxploglim2  26945  jensenlem2  26954  emcllem6  26967  harmoniclbnd  26975  harmonicubnd  26976  harmonicbnd4  26977  fsumharmonic  26978  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem5  26999  lgambdd  27003  ftalem2  27040  basellem3  27049  basellem5  27051  basellem6  27052  dvdsflsumcom  27154  fsumfldivdiaglem  27155  ppiub  27171  chtublem  27178  logfac2  27184  chpub  27187  logfacubnd  27188  logfaclbnd  27189  logfacbnd3  27190  logexprlim  27192  bcmono  27244  bpos1lem  27249  bposlem1  27251  bposlem2  27252  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem6  27256  bposlem7  27257  bposlem9  27259  lgsdirprm  27298  lgsquadlem1  27347  2lgslem1c  27360  2sqlem8  27393  chebbnd1lem1  27436  chebbnd1lem3  27438  chtppilimlem1  27440  chpchtlim  27446  vmadivsumb  27450  rplogsumlem1  27451  rplogsumlem2  27452  rpvmasumlem  27454  dchrisumlema  27455  dchrisumlem2  27457  dchrisumlem3  27458  dchrmusum2  27461  dchrvmasumlem2  27465  dchrvmasumlem3  27466  dchrvmasumlema  27467  dchrvmasumiflem1  27468  dchrisum0flblem1  27475  dchrisum0flblem2  27476  dchrisum0fno1  27478  dchrisum0re  27480  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0  27487  rplogsum  27494  mudivsum  27497  mulogsumlem  27498  logdivsum  27500  mulog2sumlem1  27501  mulog2sumlem2  27502  2vmadivsumlem  27507  log2sumbnd  27511  selberglem2  27513  selbergb  27516  selberg2lem  27517  selberg2b  27519  chpdifbndlem1  27520  logdivbnd  27523  selberg3lem1  27524  selberg3lem2  27525  selberg4lem1  27527  pntrmax  27531  pntrsumo1  27532  pntrsumbnd  27533  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntrlog2bnd  27551  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntibndlem2  27558  pntibndlem3  27559  pntlemg  27565  pntlemr  27569  pntlemj  27570  pntlemf  27572  pntlemk  27573  pntlemo  27574  pntleml  27578  abvcxp  27582  qabvle  27592  padicabv  27597  ostth2lem2  27601  ostth2lem3  27602  ostth3  27605  axlowdimlem16  29030  axcontlem8  29044  axcontlem10  29046  wwlksm1edg  29954  wwlksubclwwlk  30133  smcnlem  30772  nmoub3i  30848  ubthlem3  30947  minvecolem2  30950  minvecolem3  30951  minvecolem4  30955  htthlem  30992  bcs2  31257  pjhthlem1  31466  cnlnadjlem2  32143  cnlnadjlem7  32148  nmopadjlem  32164  nmoptrii  32169  nmopcoadji  32176  leopnmid  32213  cdj1i  32508  nndiffz1  32866  nexple  32925  oexpled  32928  pmtrto1cl  33181  psgnfzto1stlem  33182  fzto1st  33185  psgnfzto1st  33187  cyc3conja  33239  constrresqrtcl  33934  cos9thpiminplylem1  33939  smatrcl  33953  submateqlem1  33964  esumpcvgval  34235  oddpwdc  34511  eulerpartlems  34517  eulerpartlemgc  34519  eulerpartlemb  34525  dstfrvunirn  34632  orvclteinc  34633  ballotlemsima  34673  ballotlemfrcn0  34687  signstfveq0  34734  fsum2dsub  34764  breprexplemc  34789  breprexp  34790  logdivsqrle  34807  hgt750lemb  34813  hgt750leme  34815  tgoldbachgnn  34816  dnibndlem2  36679  dnibndlem6  36683  dnibndlem9  36686  dnibndlem10  36687  dnibndlem11  36688  dnibndlem12  36689  knoppcnlem4  36696  unblimceq0lem  36706  unblimceq0  36707  unbdqndv2lem2  36710  knoppndvlem11  36722  knoppndvlem14  36725  knoppndvlem15  36726  knoppndvlem18  36729  knoppndvlem21  36732  poimirlem6  37827  poimirlem7  37828  poimirlem13  37834  poimirlem15  37836  poimirlem29  37850  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  itg2addnc  37875  iblmulc2nc  37886  ftc1anclem7  37900  ftc1anclem8  37901  filbcmb  37941  geomcau  37960  prdsbnd  37994  cntotbnd  37997  bfplem2  38024  rrntotbnd  38037  iccbnd  38041  lcmineqlem20  42302  lcmineqlem21  42303  lcmineqlem22  42304  3lexlogpow5ineq2  42309  3lexlogpow5ineq5  42314  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p1p7  42328  aks4d1p1p5  42329  aks4d1p1  42330  aks4d1p2  42331  aks4d1p3  42332  aks4d1p5  42334  aks4d1p6  42335  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8  42341  posbezout  42354  aks6d1c1  42370  aks6d1c2lem4  42381  2np3bcnp1  42398  sticksstones6  42405  sticksstones7  42406  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  sticksstones22  42422  bcled  42432  bcle2d  42433  aks6d1c7lem1  42434  aks6d1c7lem2  42435  unitscyglem4  42452  lzunuz  43010  irrapxlem3  43066  irrapxlem4  43067  irrapxlem5  43068  pellexlem2  43072  pell1qrge1  43112  monotoddzzfi  43184  jm2.17a  43202  rmygeid  43206  fzmaxdif  43223  jm2.27c  43249  jm3.1lem1  43259  expdiophlem1  43263  fzunt  43696  fzuntd  43697  fzunt1d  43698  fzuntgd  43699  imo72b2lem0  44406  int-ineqtransd  44435  dvgrat  44553  monoords  45545  absnpncan2d  45550  absnpncan3d  45555  ssfiunibd  45557  rexabslelem  45662  uzublem  45674  sqrlearg  45799  fmul01  45826  fmul01lt1lem1  45830  fmul01lt1lem2  45831  climsuselem1  45853  climsuse  45854  limsupresico  45944  limsupubuzlem  45956  limsupmnfuzlem  45970  limsupre3uzlem  45979  liminfresico  46015  limsup10exlem  46016  cnrefiisplem  46073  dvdivbd  46167  dvbdfbdioolem2  46173  ioodvbdlimc1lem1  46175  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnmul  46187  dvnprodlem1  46190  dvnprodlem2  46191  iblspltprt  46217  itgspltprt  46223  stoweidlem1  46245  stoweidlem3  46247  stoweidlem5  46249  stoweidlem11  46255  stoweidlem17  46261  stoweidlem20  46264  stoweidlem26  46270  stoweidlem34  46278  wallispilem4  46312  stirlinglem11  46328  stirlinglem12  46329  stirlinglem13  46330  fourierdlem12  46363  fourierdlem15  46366  fourierdlem20  46371  fourierdlem30  46381  fourierdlem39  46390  fourierdlem42  46393  fourierdlem47  46397  fourierdlem50  46400  fourierdlem64  46414  fourierdlem65  46415  fourierdlem68  46418  fourierdlem73  46423  fourierdlem77  46427  fourierdlem79  46429  fourierdlem87  46437  elaa2lem  46477  etransclem23  46501  ioorrnopnlem  46548  salgencntex  46587  sge0le  46651  sge0isum  46671  sge0xaddlem1  46677  hoicvr  46792  hsphoidmvle2  46829  hoidmv1lelem1  46835  hoidmv1lelem2  46836  hoidmv1lelem3  46837  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem4  46842  hspmbllem1  46870  hspmbllem2  46871  smfmullem1  47035  smfmullem2  47036  smfmullem3  47037  smfsuplem1  47055  ormkglobd  47119  natglobalincr  47121  2ltceilhalf  47574  ceilhalfnn  47582  modmknepk  47608  lighneallem4a  47854  gpgusgralem  48302  gpgedgvtx1  48308  gpg3kgrtriexlem4  48332  gpg3kgrtriexlem6  48334  fllog2  48814  itcovalt2lem2lem1  48919