Theorem letrd 11273

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008   ≤ cle 11150

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-pre-lttri 11083  ax-pre-lttrn 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155

This theorem is referenced by:  lesub3d  11738  le2addd  11739  supmul1  12094  supmul  12097  nn0negleid  12436  eluzuzle  12744  iccsplit  13388  supicc  13404  fzdisj  13454  ssfzunsnext  13472  difelfzle  13544  flwordi  13716  flleceil  13757  uzsup  13767  modltm1p1mod  13830  seqf1olem1  13948  zzlesq  14113  bernneq  14136  bernneq3  14138  discr1  14146  faclbnd  14197  faclbnd4lem1  14200  facubnd  14207  seqcoll  14371  01sqrexlem7  15155  absle  15223  releabs  15229  absrdbnd  15249  rexuzre  15260  limsupgre  15388  lo1bddrp  15432  rlimclim1  15452  rlimresb  15472  rlimrege0  15486  o1add  15521  o1sub  15523  climsqz  15548  climsqz2  15549  rlimsqzlem  15556  rlimsqz  15557  rlimsqz2  15558  rlimno1  15561  isercoll  15575  caucvgrlem  15580  iseraltlem3  15591  o1fsum  15720  cvgcmp  15723  cvgcmpce  15725  climcnds  15758  expcnv  15771  cvgrat  15790  mertenslem2  15792  fprodle  15903  eftlub  16018  rpnnen2lem12  16134  bitsfzo  16346  isprm5  16618  isprm7  16619  eulerthlem2  16693  pcmpt2  16805  pcfac  16811  prmreclem3  16830  prmreclem4  16831  prmreclem5  16832  4sqlem11  16867  vdwlem1  16893  vdwlem3  16895  setsstruct2  17085  prdsxmetlem  24254  nrmmetd  24460  nm2dif  24511  nlmvscnlem2  24571  nmoco  24623  nmotri  24625  nghmcn  24631  icccmplem2  24710  reconnlem2  24714  elii1  24829  xrhmeo  24842  cnheiborlem  24851  bndth  24855  tcphcphlem1  25133  ipcnlem2  25142  cncmet  25220  trirn  25298  minveclem2  25324  minveclem4  25330  ivthlem2  25351  ovolunlem1a  25395  ovolunlem1  25396  ovolfiniun  25400  ovoliunlem1  25401  ovolicc2lem4  25419  ovolicc2lem5  25420  ovolicopnf  25423  nulmbl2  25435  ioombl1lem4  25460  ioorcl2  25471  uniioombllem3  25484  uniioombllem4  25485  uniioombllem5  25486  volcn  25505  vitalilem2  25508  vitali  25512  mbfi1fseqlem5  25618  mbfi1fseqlem6  25619  itg2splitlem  25647  itg2monolem1  25649  itg2monolem3  25651  itg2mono  25652  itg2cnlem1  25660  itgle  25709  bddmulibl  25738  bddiblnc  25741  ditgsplitlem  25759  dveflem  25881  dvlip  25896  dveq0  25903  dvfsumabs  25927  dvfsumlem1  25930  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem3  25933  dvfsumlem4  25934  dvfsum2  25939  fta1glem2  26072  dgradd2  26172  plydiveu  26204  fta1lem  26213  aalioulem2  26239  aalioulem3  26240  aalioulem4  26241  aalioulem5  26242  aaliou3lem8  26251  aaliou3lem9  26256  ulmbdd  26305  ulmcn  26306  mtest  26311  mtestbdd  26312  abelthlem2  26340  abelthlem7  26346  pilem2  26360  tanabsge  26413  cosordlem  26437  tanord  26445  logneg2  26522  abslogle  26525  dvlog2lem  26559  cxple2a  26606  abscxpbnd  26661  atans2  26839  leibpi  26850  o1cxp  26883  cxploglim2  26887  jensenlem2  26896  emcllem6  26909  harmoniclbnd  26917  harmonicubnd  26918  harmonicbnd4  26919  fsumharmonic  26920  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamgulmlem5  26941  lgambdd  26945  ftalem2  26982  basellem3  26991  basellem5  26993  basellem6  26994  dvdsflsumcom  27096  fsumfldivdiaglem  27097  ppiub  27113  chtublem  27120  logfac2  27126  chpub  27129  logfacubnd  27130  logfaclbnd  27131  logfacbnd3  27132  logexprlim  27134  bcmono  27186  bpos1lem  27191  bposlem1  27193  bposlem2  27194  bposlem3  27195  bposlem4  27196  bposlem5  27197  bposlem6  27198  bposlem7  27199  bposlem9  27201  lgsdirprm  27240  lgsquadlem1  27289  2lgslem1c  27302  2sqlem8  27335  chebbnd1lem1  27378  chebbnd1lem3  27380  chtppilimlem1  27382  chpchtlim  27388  vmadivsumb  27392  rplogsumlem1  27393  rplogsumlem2  27394  rpvmasumlem  27396  dchrisumlema  27397  dchrisumlem2  27399  dchrisumlem3  27400  dchrmusum2  27403  dchrvmasumlem2  27407  dchrvmasumlem3  27408  dchrvmasumlema  27409  dchrvmasumiflem1  27410  dchrisum0flblem1  27417  dchrisum0flblem2  27418  dchrisum0fno1  27420  dchrisum0re  27422  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0  27429  rplogsum  27436  mudivsum  27439  mulogsumlem  27440  logdivsum  27442  mulog2sumlem1  27443  mulog2sumlem2  27444  2vmadivsumlem  27449  log2sumbnd  27453  selberglem2  27455  selbergb  27458  selberg2lem  27459  selberg2b  27461  chpdifbndlem1  27462  logdivbnd  27465  selberg3lem1  27466  selberg3lem2  27467  selberg4lem1  27469  pntrmax  27473  pntrsumo1  27474  pntrsumbnd  27475  pntrlog2bndlem1  27486  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntrlog2bnd  27493  pntpbnd1a  27494  pntpbnd1  27495  pntpbnd2  27496  pntibndlem2  27500  pntibndlem3  27501  pntlemg  27507  pntlemr  27511  pntlemj  27512  pntlemf  27514  pntlemk  27515  pntlemo  27516  pntleml  27520  abvcxp  27524  qabvle  27534  padicabv  27539  ostth2lem2  27543  ostth2lem3  27544  ostth3  27547  axlowdimlem16  28902  axcontlem8  28916  axcontlem10  28918  wwlksm1edg  29826  wwlksubclwwlk  30002  smcnlem  30641  nmoub3i  30717  ubthlem3  30816  minvecolem2  30819  minvecolem3  30820  minvecolem4  30824  htthlem  30861  bcs2  31126  pjhthlem1  31335  cnlnadjlem2  32012  cnlnadjlem7  32017  nmopadjlem  32033  nmoptrii  32038  nmopcoadji  32045  leopnmid  32082  cdj1i  32377  nndiffz1  32729  nexple  32789  oexpled  32792  pmtrto1cl  33041  psgnfzto1stlem  33042  fzto1st  33045  psgnfzto1st  33047  cyc3conja  33099  constrresqrtcl  33744  cos9thpiminplylem1  33749  smatrcl  33763  submateqlem1  33774  esumpcvgval  34045  oddpwdc  34322  eulerpartlems  34328  eulerpartlemgc  34330  eulerpartlemb  34336  dstfrvunirn  34443  orvclteinc  34444  ballotlemsima  34484  ballotlemfrcn0  34498  signstfveq0  34545  fsum2dsub  34575  breprexplemc  34600  breprexp  34601  logdivsqrle  34618  hgt750lemb  34624  hgt750leme  34626  tgoldbachgnn  34627  dnibndlem2  36453  dnibndlem6  36457  dnibndlem9  36460  dnibndlem10  36461  dnibndlem11  36462  dnibndlem12  36463  knoppcnlem4  36470  unblimceq0lem  36480  unblimceq0  36481  unbdqndv2lem2  36484  knoppndvlem11  36496  knoppndvlem14  36499  knoppndvlem15  36500  knoppndvlem18  36503  knoppndvlem21  36506  poimirlem6  37606  poimirlem7  37607  poimirlem13  37613  poimirlem15  37615  poimirlem29  37629  mblfinlem2  37638  mblfinlem3  37639  mblfinlem4  37640  ismblfin  37641  itg2addnc  37654  iblmulc2nc  37665  ftc1anclem7  37679  ftc1anclem8  37680  filbcmb  37720  geomcau  37739  prdsbnd  37773  cntotbnd  37776  bfplem2  37803  rrntotbnd  37816  iccbnd  37820  lcmineqlem20  42021  lcmineqlem21  42022  lcmineqlem22  42023  3lexlogpow5ineq2  42028  3lexlogpow5ineq5  42033  aks4d1p1p2  42043  aks4d1p1p4  42044  aks4d1p1p7  42047  aks4d1p1p5  42048  aks4d1p1  42049  aks4d1p2  42050  aks4d1p3  42051  aks4d1p5  42053  aks4d1p6  42054  aks4d1p7d1  42055  aks4d1p7  42056  aks4d1p8  42060  posbezout  42073  aks6d1c1  42089  aks6d1c2lem4  42100  2np3bcnp1  42117  sticksstones6  42124  sticksstones7  42125  sticksstones10  42128  sticksstones12a  42130  sticksstones12  42131  sticksstones22  42141  bcled  42151  bcle2d  42152  aks6d1c7lem1  42153  aks6d1c7lem2  42154  unitscyglem4  42171  lzunuz  42741  irrapxlem3  42797  irrapxlem4  42798  irrapxlem5  42799  pellexlem2  42803  pell1qrge1  42843  monotoddzzfi  42915  jm2.17a  42933  rmygeid  42937  fzmaxdif  42954  jm2.27c  42980  jm3.1lem1  42990  expdiophlem1  42994  fzunt  43428  fzuntd  43429  fzunt1d  43430  fzuntgd  43431  imo72b2lem0  44138  int-ineqtransd  44167  dvgrat  44285  monoords  45279  absnpncan2d  45284  absnpncan3d  45289  ssfiunibd  45291  rexabslelem  45397  uzublem  45409  sqrlearg  45534  fmul01  45561  fmul01lt1lem1  45565  fmul01lt1lem2  45566  climsuselem1  45588  climsuse  45589  limsupresico  45681  limsupubuzlem  45693  limsupmnfuzlem  45707  limsupre3uzlem  45716  liminfresico  45752  limsup10exlem  45753  cnrefiisplem  45810  dvdivbd  45904  dvbdfbdioolem2  45910  ioodvbdlimc1lem1  45912  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  dvnmul  45924  dvnprodlem1  45927  dvnprodlem2  45928  iblspltprt  45954  itgspltprt  45960  stoweidlem1  45982  stoweidlem3  45984  stoweidlem5  45986  stoweidlem11  45992  stoweidlem17  45998  stoweidlem20  46001  stoweidlem26  46007  stoweidlem34  46015  wallispilem4  46049  stirlinglem11  46065  stirlinglem12  46066  stirlinglem13  46067  fourierdlem12  46100  fourierdlem15  46103  fourierdlem20  46108  fourierdlem30  46118  fourierdlem39  46127  fourierdlem42  46130  fourierdlem47  46134  fourierdlem50  46137  fourierdlem64  46151  fourierdlem65  46152  fourierdlem68  46155  fourierdlem73  46160  fourierdlem77  46164  fourierdlem79  46166  fourierdlem87  46174  elaa2lem  46214  etransclem23  46238  ioorrnopnlem  46285  salgencntex  46324  sge0le  46388  sge0isum  46408  sge0xaddlem1  46414  hoicvr  46529  hsphoidmvle2  46566  hoidmv1lelem1  46572  hoidmv1lelem2  46573  hoidmv1lelem3  46574  hoidmvlelem1  46576  hoidmvlelem2  46577  hoidmvlelem4  46579  hspmbllem1  46607  hspmbllem2  46608  smfmullem1  46772  smfmullem2  46773  smfmullem3  46774  smfsuplem1  46792  ormkglobd  46856  natglobalincr  46858  2ltceilhalf  47312  ceilhalfnn  47320  modmknepk  47346  lighneallem4a  47592  gpgusgralem  48040  gpgedgvtx1  48046  gpg3kgrtriexlem4  48070  gpg3kgrtriexlem6  48072  fllog2  48553  itcovalt2lem2lem1  48658