Theorem letrd 11408

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098   class class class wbr 5149  ℝcr 11144   ≤ cle 11286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11202  ax-pre-lttri 11219  ax-pre-lttrn 11220

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291

This theorem is referenced by:  lesub3d  11869  supmul1  12221  supmul  12224  nn0negleid  12562  eluzuzle  12869  iccsplit  13502  supicc  13518  fzdisj  13568  ssfzunsnext  13586  difelfzle  13654  flwordi  13818  flleceil  13859  uzsup  13869  modltm1p1mod  13929  seqf1olem1  14047  zzlesq  14210  bernneq  14232  bernneq3  14234  discr1  14242  faclbnd  14290  faclbnd4lem1  14293  facubnd  14300  seqcoll  14466  01sqrexlem7  15236  absle  15303  releabs  15309  absrdbnd  15329  rexuzre  15340  limsupgre  15466  lo1bddrp  15510  rlimclim1  15530  rlimresb  15550  rlimrege0  15564  o1add  15599  o1sub  15601  climsqz  15626  climsqz2  15627  rlimsqzlem  15636  rlimsqz  15637  rlimsqz2  15638  rlimno1  15641  isercoll  15655  caucvgrlem  15660  iseraltlem3  15671  o1fsum  15800  cvgcmp  15803  cvgcmpce  15805  climcnds  15838  expcnv  15851  cvgrat  15870  mertenslem2  15872  fprodle  15981  eftlub  16094  rpnnen2lem12  16210  bitsfzo  16418  isprm5  16686  isprm7  16687  eulerthlem2  16759  pcmpt2  16870  pcfac  16876  prmreclem3  16895  prmreclem4  16896  prmreclem5  16897  4sqlem11  16932  vdwlem1  16958  vdwlem3  16960  setsstruct2  17151  prdsxmetlem  24323  nrmmetd  24532  nm2dif  24583  nlmvscnlem2  24651  nmoco  24703  nmotri  24705  nghmcn  24711  icccmplem2  24788  reconnlem2  24792  elii1  24907  xrhmeo  24920  cnheiborlem  24929  bndth  24933  tcphcphlem1  25212  ipcnlem2  25221  cncmet  25299  trirn  25377  minveclem2  25403  minveclem4  25409  ivthlem2  25430  ovolunlem1a  25474  ovolunlem1  25475  ovolfiniun  25479  ovoliunlem1  25480  ovolicc2lem4  25498  ovolicc2lem5  25499  ovolicopnf  25502  nulmbl2  25514  ioombl1lem4  25539  ioorcl2  25550  uniioombllem3  25563  uniioombllem4  25564  uniioombllem5  25565  volcn  25584  vitalilem2  25587  vitali  25591  mbfi1fseqlem5  25698  mbfi1fseqlem6  25699  itg2splitlem  25727  itg2monolem1  25729  itg2monolem3  25731  itg2mono  25732  itg2cnlem1  25740  itgle  25788  bddmulibl  25817  bddiblnc  25820  ditgsplitlem  25838  dveflem  25960  dvlip  25975  dveq0  25982  dvfsumabs  26006  dvfsumlem1  26009  dvfsumlem2  26010  dvfsumlem2OLD  26011  dvfsumlem3  26012  dvfsumlem4  26013  dvfsum2  26018  fta1glem2  26153  dgradd2  26253  plydiveu  26283  fta1lem  26292  aalioulem2  26318  aalioulem3  26319  aalioulem4  26320  aalioulem5  26321  aaliou3lem8  26330  aaliou3lem9  26335  ulmbdd  26384  ulmcn  26385  mtest  26390  mtestbdd  26391  abelthlem2  26419  abelthlem7  26425  pilem2  26439  tanabsge  26491  cosordlem  26514  tanord  26522  logneg2  26599  abslogle  26602  dvlog2lem  26636  cxple2a  26683  abscxpbnd  26738  atans2  26913  leibpi  26924  o1cxp  26957  cxploglim2  26961  jensenlem2  26970  emcllem6  26983  harmoniclbnd  26991  harmonicubnd  26992  harmonicbnd4  26993  fsumharmonic  26994  lgamgulmlem2  27012  lgamgulmlem3  27013  lgamgulmlem5  27015  lgambdd  27019  ftalem2  27056  basellem3  27065  basellem5  27067  basellem6  27068  dvdsflsumcom  27170  fsumfldivdiaglem  27171  ppiub  27187  chtublem  27194  logfac2  27200  chpub  27203  logfacubnd  27204  logfaclbnd  27205  logfacbnd3  27206  logexprlim  27208  bcmono  27260  bpos1lem  27265  bposlem1  27267  bposlem2  27268  bposlem3  27269  bposlem4  27270  bposlem5  27271  bposlem6  27272  bposlem7  27273  bposlem9  27275  lgsdirprm  27314  lgsquadlem1  27363  2lgslem1c  27376  2sqlem8  27409  chebbnd1lem1  27452  chebbnd1lem3  27454  chtppilimlem1  27456  chpchtlim  27462  vmadivsumb  27466  rplogsumlem1  27467  rplogsumlem2  27468  rpvmasumlem  27470  dchrisumlema  27471  dchrisumlem2  27473  dchrisumlem3  27474  dchrmusum2  27477  dchrvmasumlem2  27481  dchrvmasumlem3  27482  dchrvmasumlema  27483  dchrvmasumiflem1  27484  dchrisum0flblem1  27491  dchrisum0flblem2  27492  dchrisum0fno1  27494  dchrisum0re  27496  dchrisum0lem1b  27498  dchrisum0lem1  27499  dchrisum0lem2a  27500  dchrisum0  27503  rplogsum  27510  mudivsum  27513  mulogsumlem  27514  logdivsum  27516  mulog2sumlem1  27517  mulog2sumlem2  27518  2vmadivsumlem  27523  log2sumbnd  27527  selberglem2  27529  selbergb  27532  selberg2lem  27533  selberg2b  27535  chpdifbndlem1  27536  logdivbnd  27539  selberg3lem1  27540  selberg3lem2  27541  selberg4lem1  27543  pntrmax  27547  pntrsumo1  27548  pntrsumbnd  27549  pntrlog2bndlem1  27560  pntrlog2bndlem2  27561  pntrlog2bndlem3  27562  pntrlog2bndlem5  27564  pntrlog2bndlem6  27566  pntrlog2bnd  27567  pntpbnd1a  27568  pntpbnd1  27569  pntpbnd2  27570  pntibndlem2  27574  pntibndlem3  27575  pntlemg  27581  pntlemr  27585  pntlemj  27586  pntlemf  27588  pntlemk  27589  pntlemo  27590  pntleml  27594  abvcxp  27598  qabvle  27608  padicabv  27613  ostth2lem2  27617  ostth2lem3  27618  ostth3  27621  axlowdimlem16  28845  axcontlem8  28859  axcontlem10  28861  wwlksm1edg  29769  wwlksubclwwlk  29945  smcnlem  30584  nmoub3i  30660  ubthlem3  30759  minvecolem2  30762  minvecolem3  30763  minvecolem4  30767  htthlem  30804  bcs2  31069  pjhthlem1  31278  cnlnadjlem2  31955  cnlnadjlem7  31960  nmopadjlem  31976  nmoptrii  31981  nmopcoadji  31988  leopnmid  32025  cdj1i  32320  nndiffz1  32641  pmtrto1cl  32917  psgnfzto1stlem  32918  fzto1st  32921  psgnfzto1st  32923  cyc3conja  32975  smatrcl  33530  submateqlem1  33541  nexple  33761  esumpcvgval  33830  oddpwdc  34107  eulerpartlems  34113  eulerpartlemgc  34115  eulerpartlemb  34121  dstfrvunirn  34227  orvclteinc  34228  ballotlemsima  34268  ballotlemfrcn0  34282  signstfveq0  34342  fsum2dsub  34372  breprexplemc  34397  breprexp  34398  logdivsqrle  34415  hgt750lemb  34421  hgt750leme  34423  tgoldbachgnn  34424  dnibndlem2  36087  dnibndlem6  36091  dnibndlem9  36094  dnibndlem10  36095  dnibndlem11  36096  dnibndlem12  36097  knoppcnlem4  36104  unblimceq0lem  36114  unblimceq0  36115  unbdqndv2lem2  36118  knoppndvlem11  36130  knoppndvlem14  36133  knoppndvlem15  36134  knoppndvlem18  36137  knoppndvlem21  36140  poimirlem6  37232  poimirlem7  37233  poimirlem13  37239  poimirlem15  37241  poimirlem29  37255  mblfinlem2  37264  mblfinlem3  37265  mblfinlem4  37266  ismblfin  37267  itg2addnc  37280  iblmulc2nc  37291  ftc1anclem7  37305  ftc1anclem8  37306  filbcmb  37346  geomcau  37365  prdsbnd  37399  cntotbnd  37402  bfplem2  37429  rrntotbnd  37442  iccbnd  37446  lcmineqlem20  41653  lcmineqlem21  41654  lcmineqlem22  41655  3lexlogpow5ineq2  41660  3lexlogpow5ineq5  41665  aks4d1p1p2  41675  aks4d1p1p4  41676  aks4d1p1p7  41679  aks4d1p1p5  41680  aks4d1p1  41681  aks4d1p2  41682  aks4d1p3  41683  aks4d1p5  41685  aks4d1p6  41686  aks4d1p7d1  41687  aks4d1p7  41688  aks4d1p8  41692  posbezout  41705  aks6d1c1  41721  aks6d1c2lem4  41732  2np3bcnp1  41749  sticksstones6  41756  sticksstones7  41757  sticksstones10  41760  sticksstones12a  41762  sticksstones12  41763  sticksstones22  41773  bcled  41783  bcle2d  41784  aks6d1c7lem1  41785  aks6d1c7lem2  41786  metakunt1  41793  metakunt12  41804  metakunt28  41820  lzunuz  42332  irrapxlem3  42388  irrapxlem4  42389  irrapxlem5  42390  pellexlem2  42394  pell1qrge1  42434  monotoddzzfi  42507  jm2.17a  42525  rmygeid  42529  fzmaxdif  42546  jm2.27c  42572  jm3.1lem1  42582  expdiophlem1  42586  fzunt  43029  fzuntd  43030  fzunt1d  43031  fzuntgd  43032  imo72b2lem0  43739  int-ineqtransd  43768  dvgrat  43893  monoords  44819  absnpncan2d  44824  absnpncan3d  44829  ssfiunibd  44831  leadd12dd  44838  rexabslelem  44940  uzublem  44952  sqrlearg  45078  fmul01  45108  fmul01lt1lem1  45112  fmul01lt1lem2  45113  climsuselem1  45135  climsuse  45136  limsupresico  45228  limsupubuzlem  45240  limsupmnfuzlem  45254  limsupre3uzlem  45263  liminfresico  45299  limsup10exlem  45300  cnrefiisplem  45357  dvdivbd  45451  dvbdfbdioolem2  45457  ioodvbdlimc1lem1  45459  ioodvbdlimc1lem2  45460  ioodvbdlimc2lem  45462  dvnmul  45471  dvnprodlem1  45474  dvnprodlem2  45475  iblspltprt  45501  itgspltprt  45507  stoweidlem1  45529  stoweidlem3  45531  stoweidlem5  45533  stoweidlem11  45539  stoweidlem17  45545  stoweidlem20  45548  stoweidlem26  45554  stoweidlem34  45562  wallispilem4  45596  stirlinglem11  45612  stirlinglem12  45613  stirlinglem13  45614  fourierdlem12  45647  fourierdlem15  45650  fourierdlem20  45655  fourierdlem30  45665  fourierdlem39  45674  fourierdlem42  45677  fourierdlem47  45681  fourierdlem50  45684  fourierdlem64  45698  fourierdlem65  45699  fourierdlem68  45702  fourierdlem73  45707  fourierdlem77  45711  fourierdlem79  45713  fourierdlem87  45721  elaa2lem  45761  etransclem23  45785  ioorrnopnlem  45832  salgencntex  45871  sge0le  45935  sge0isum  45955  sge0xaddlem1  45961  hoicvr  46076  hsphoidmvle2  46113  hoidmv1lelem1  46119  hoidmv1lelem2  46120  hoidmv1lelem3  46121  hoidmvlelem1  46123  hoidmvlelem2  46124  hoidmvlelem4  46126  hspmbllem1  46154  hspmbllem2  46155  smfmullem1  46319  smfmullem2  46320  smfmullem3  46321  smfsuplem1  46339  natglobalincr  46403  lighneallem4a  47087  fllog2  47829  itcovalt2lem2lem1  47934