Theorem addcld 11126

Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
addcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Proof of Theorem addcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addcl 11083	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7341  ℂcc 10999   + caddc 11004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 11061

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  cnegex  11289  addcom  11294  addcomd  11310  muladd11r  11321  negeu  11345  addsubass  11365  subsub2  11384  subsub4  11389  pnncan  11397  addsub4  11399  addsubsub23  11520  pnpncand  11533  addmulsub  11574  subaddmulsub  11575  mulsubaddmulsub  11576  divdir  11796  cju  12116  cnref1o  12878  xov1plusxeqvd  13393  modaddb  13808  expaddz  14008  binom3  14126  sqoddm1div8  14145  mulsubdivbinom2  14164  muldivbinom2  14165  spllen  14656  crre  15016  remullem  15030  imval2  15053  cjreim2  15063  sqreulem  15262  bhmafibid1cn  15368  bhmafibid2cn  15369  bhmafibid1  15370  bhmafibid2  15371  addcn2  15496  o1add  15516  rlimadd  15545  fsumadd  15642  isumadd  15669  binomlem  15731  binomfallfaclem2  15942  bpoly4  15961  fsumcube  15962  efaddlem  15995  ef4p  16017  cosf  16029  tanval2  16037  tanval3  16038  resin4p  16042  recos4p  16043  efival  16056  sinadd  16068  cosadd  16069  tanadd  16071  pwp1fsum  16297  sadadd2lem2  16356  sadadd2lem  16365  pythagtriplem1  16723  pythagtriplem12  16733  pythagtriplem17  16738  pcbc  16807  mul4sqlem  16860  4sqlem14  16865  vdwlem6  16893  vdwlem9  16896  mulgdirlem  19013  blcvx  24708  cphpyth  25138  tcphcphlem1  25157  cphipval2  25163  4cphipval2  25164  csbren  25321  ovollb2lem  25411  mbfadd  25584  itgcnlem  25713  itgaddlem2  25747  dvmptre  25895  dvsincos  25907  itgpowd  25979  taylthlem2  26304  taylthlem2OLD  26305  ptolemy  26427  tanregt0  26470  eff1olem  26479  cosargd  26539  tanarg  26550  logf1o2  26581  efopn  26589  cxpsqrtlem  26633  cxpeq  26689  ang180lem1  26741  ang180lem2  26742  ang180lem3  26743  ang180lem4  26744  pythag  26749  ssscongptld  26754  chordthmlem  26764  chordthmlem2  26765  chordthmlem3  26766  chordthmlem4  26767  chordthmlem5  26768  heron  26770  quad2  26771  dcubic1lem  26775  dcubic2  26776  dcubic1  26777  dcubic  26778  mcubic  26779  cubic2  26780  cubic  26781  binom4  26782  dquartlem1  26783  dquartlem2  26784  dquart  26785  quart1cl  26786  quart1lem  26787  quart1  26788  quartlem1  26789  quartlem2  26790  quartlem3  26791  quartlem4  26792  quart  26793  asinlem3  26803  asinf  26804  asinneg  26818  efiasin  26820  asinsinlem  26823  asinsin  26824  asinbnd  26831  atanlogaddlem  26845  dmgmaddnn0  26959  dmgmdivn0  26960  lgamgulmlem2  26962  lgamgulmlem3  26963  lgamgulmlem4  26964  lgamgulmlem5  26965  lgamgulmlem6  26966  lgamgulm2  26968  lgambdd  26969  lgamucov  26970  lgamcvg2  26987  gamcvg  26988  gamcvg2lem  26991  ftalem7  27011  basellem3  27015  bposlem9  27225  lgsquad2lem1  27317  2lgslem3d1  27336  2sqmod  27369  dchrvmasumiflem2  27435  mulogsumlem  27464  mulog2sumlem1  27467  mulog2sumlem2  27468  mulog2sumlem3  27469  selberglem1  27478  selberg2  27484  selberg3lem1  27490  selbergr  27501  selberg3r  27502  pntrlog2bndlem1  27510  pntrlog2bndlem2  27511  pntrlog2bndlem5  27514  pntrlog2bndlem6  27516  pntrlog2bnd  27517  brbtwn2  28878  colinearalglem1  28879  colinearalglem2  28880  axeuclidlem  28935  axcontlem2  28938  axcontlem7  28943  axcontlem8  28944  finsumvtxdg2ssteplem4  29522  wwlksext2clwwlk  30029  4ipval2  30680  dipcj  30686  golem1  32243  submuladdd  32715  binom2subadd  32717  pythagreim  32721  quad3d  32725  lt2addrd  32726  cycpmco2lem3  33089  cycpmco2lem4  33090  cycpmco2lem5  33091  cycpmco2lem6  33092  cycpmco2  33094  archirngz  33150  archiabllem2c  33156  zringfrac  33511  ccfldextdgrr  33677  constrrtll  33736  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  constrfin  33751  nn0constr  33766  constraddcl  33767  constrrecl  33774  constrresqrtcl  33782  constrsqrtcl  33784  cos9thpiminplylem1  33787  cos9thpiminplylem2  33788  cos9thpiminplylem3  33789  cos9thpiminply  33793  cos9thpinconstrlem1  33794  cos9thpinconstrlem2  33795  cnre2csqima  33916  ballotlemsima  34521  hgt750lemb  34661  iprodgam  35778  dnizphlfeqhlf  36510  dnibndlem9  36520  knoppndvlem16  36561  itg2addnclem3  37713  itgaddnclem2  37719  itgaddnc  37720  ftc1anclem6  37738  ftc1anclem8  37740  dvasin  37744  areacirclem1  37748  areacirclem4  37751  areacirc  37753  lcmineqlem6  42067  lcmineqlem11  42072  lcmineqlem18  42079  aks4d1p1p2  42103  aks4d1p1p6  42106  aks4d1p1p7  42107  aks4d1p1p5  42108  posbezout  42133  2np3bcnp1  42177  2ap1caineq  42178  sticksstones12a  42190  bcle2d  42212  mvrrsubd  42307  lsubrotld  42310  oddnumth  42344  sumcubes  42346  cxp112d  42374  cxp111d  42375  sn-negex12  42450  sn-addrid  42454  sn-subeu  42460  sn-0tie0  42484  zaddcomlem  42496  zaddcom  42497  cnreeu  42523  dffltz  42667  cu3addd  42714  3cubeslem2  42718  3cubeslem3l  42719  3cubeslem3r  42720  3cubeslem4  42722  pellexlem2  42863  pellexlem6  42867  pell1234qrreccl  42887  pell1234qrmulcl  42888  pell14qrdich  42902  rmxyneg  42953  rmxyadd  42954  jm2.19lem4  43025  jm2.26lem3  43034  sqrtcval  43674  int-rightdistd  44213  binomcxplemnn0  44382  binomcxplemrat  44383  binomcxplemfrat  44384  binomcxplemdvbinom  44386  binomcxplemnotnn0  44389  sub2times  45314  clim1fr1  45641  limcperiod  45668  addlimc  45686  coseq0  45902  fprodaddrecnncnvlem  45947  dvxpaek  45978  dvnxpaek  45980  dvnmul  45981  itgiccshift  46018  itgperiod  46019  stoweidlem1  46039  stoweidlem11  46049  stoweidlem13  46051  wallispilem4  46106  wallispilem5  46107  wallispi  46108  wallispi2lem1  46109  wallispi2lem2  46110  wallispi2  46111  stirlinglem1  46112  stirlinglem3  46114  stirlinglem4  46115  stirlinglem5  46116  stirlinglem6  46117  stirlinglem7  46118  stirlinglem10  46121  stirlinglem11  46122  stirlinglem12  46123  stirlinglem13  46124  stirlinglem15  46126  dirkerper  46134  dirkertrigeqlem1  46136  dirkertrigeqlem2  46137  dirkertrigeqlem3  46138  dirkeritg  46140  dirkercncflem2  46142  dirkercncflem4  46144  fourierdlem18  46163  fourierdlem26  46171  fourierdlem30  46175  fourierdlem48  46192  fourierdlem49  46193  fourierdlem79  46223  fourierdlem83  46227  fourierdlem92  46236  fourierdlem93  46237  fourierdlem103  46247  fourierdlem104  46248  fourierdlem111  46255  fourierdlem112  46256  smfmullem1  46829  sigaraf  46891  sigaras  46893  readdcnnred  47334  fldivmod  47369  fmtnorec4  47580  quad1  47651  requad01  47652  requad2  47654  gpgedgvtx1  48093  dignn0flhalflem1  48647  affinecomb2  48735  eenglngeehlnmlem1  48769  itschlc0yqe  48792  itsclc0yqsollem1  48794  itsclc0yqsol  48796  itscnhlc0xyqsol  48797  itsclc0xyqsolr  48801  2itscplem3  48812  itscnhlinecirc02plem1  48814  inlinecirc02plem  48818  sinhpcosh  49772