Theorem addcld 11134

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 11091	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   + caddc 11012

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

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

This theorem is referenced by:  cnegex  11297  addcom  11302  addcomd  11318  muladd11r  11329  negeu  11353  addsubass  11373  subsub2  11392  subsub4  11397  pnncan  11405  addsub4  11407  addsubsub23  11528  pnpncand  11541  addmulsub  11582  subaddmulsub  11583  mulsubaddmulsub  11584  divdir  11804  cju  12124  cnref1o  12886  xov1plusxeqvd  13401  modaddb  13813  expaddz  14013  binom3  14131  sqoddm1div8  14150  mulsubdivbinom2  14169  muldivbinom2  14170  spllen  14660  crre  15021  remullem  15035  imval2  15058  cjreim2  15068  sqreulem  15267  bhmafibid1cn  15373  bhmafibid2cn  15374  bhmafibid1  15375  bhmafibid2  15376  addcn2  15501  o1add  15521  rlimadd  15550  fsumadd  15647  isumadd  15674  binomlem  15736  binomfallfaclem2  15947  bpoly4  15966  fsumcube  15967  efaddlem  16000  ef4p  16022  cosf  16034  tanval2  16042  tanval3  16043  resin4p  16047  recos4p  16048  efival  16061  sinadd  16073  cosadd  16074  tanadd  16076  pwp1fsum  16302  sadadd2lem2  16361  sadadd2lem  16370  pythagtriplem1  16728  pythagtriplem12  16738  pythagtriplem17  16743  pcbc  16812  mul4sqlem  16865  4sqlem14  16870  vdwlem6  16898  vdwlem9  16901  mulgdirlem  18984  blcvx  24684  cphpyth  25114  tcphcphlem1  25133  cphipval2  25139  4cphipval2  25140  csbren  25297  ovollb2lem  25387  mbfadd  25560  itgcnlem  25689  itgaddlem2  25723  dvmptre  25871  dvsincos  25883  itgpowd  25955  taylthlem2  26280  taylthlem2OLD  26281  ptolemy  26403  tanregt0  26446  eff1olem  26455  cosargd  26515  tanarg  26526  logf1o2  26557  efopn  26565  cxpsqrtlem  26609  cxpeq  26665  ang180lem1  26717  ang180lem2  26718  ang180lem3  26719  ang180lem4  26720  pythag  26725  ssscongptld  26730  chordthmlem  26740  chordthmlem2  26741  chordthmlem3  26742  chordthmlem4  26743  chordthmlem5  26744  heron  26746  quad2  26747  dcubic1lem  26751  dcubic2  26752  dcubic1  26753  dcubic  26754  mcubic  26755  cubic2  26756  cubic  26757  binom4  26758  dquartlem1  26759  dquartlem2  26760  dquart  26761  quart1cl  26762  quart1lem  26763  quart1  26764  quartlem1  26765  quartlem2  26766  quartlem3  26767  quartlem4  26768  quart  26769  asinlem3  26779  asinf  26780  asinneg  26794  efiasin  26796  asinsinlem  26799  asinsin  26800  asinbnd  26807  atanlogaddlem  26821  dmgmaddnn0  26935  dmgmdivn0  26936  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamgulmlem4  26940  lgamgulmlem5  26941  lgamgulmlem6  26942  lgamgulm2  26944  lgambdd  26945  lgamucov  26946  lgamcvg2  26963  gamcvg  26964  gamcvg2lem  26967  ftalem7  26987  basellem3  26991  bposlem9  27201  lgsquad2lem1  27293  2lgslem3d1  27312  2sqmod  27345  dchrvmasumiflem2  27411  mulogsumlem  27440  mulog2sumlem1  27443  mulog2sumlem2  27444  mulog2sumlem3  27445  selberglem1  27454  selberg2  27460  selberg3lem1  27466  selbergr  27477  selberg3r  27478  pntrlog2bndlem1  27486  pntrlog2bndlem2  27487  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntrlog2bnd  27493  brbtwn2  28850  colinearalglem1  28851  colinearalglem2  28852  axeuclidlem  28907  axcontlem2  28910  axcontlem7  28915  axcontlem8  28916  finsumvtxdg2ssteplem4  29494  wwlksext2clwwlk  30001  4ipval2  30652  dipcj  30658  golem1  32215  submuladdd  32683  binom2subadd  32685  pythagreim  32689  quad3d  32693  lt2addrd  32694  cycpmco2lem3  33070  cycpmco2lem4  33071  cycpmco2lem5  33072  cycpmco2lem6  33073  cycpmco2  33075  archirngz  33131  archiabllem2c  33137  zringfrac  33491  ccfldextdgrr  33639  constrrtll  33698  constrrtlc1  33699  constrrtcclem  33701  constrrtcc  33702  constrfin  33713  nn0constr  33728  constraddcl  33729  constrrecl  33736  constrresqrtcl  33744  constrsqrtcl  33746  cos9thpiminplylem1  33749  cos9thpiminplylem2  33750  cos9thpiminplylem3  33751  cos9thpiminply  33755  cos9thpinconstrlem1  33756  cos9thpinconstrlem2  33757  cnre2csqima  33878  ballotlemsima  34484  hgt750lemb  34624  iprodgam  35715  dnizphlfeqhlf  36450  dnibndlem9  36460  knoppndvlem16  36501  itg2addnclem3  37653  itgaddnclem2  37659  itgaddnc  37660  ftc1anclem6  37678  ftc1anclem8  37680  dvasin  37684  areacirclem1  37688  areacirclem4  37691  areacirc  37693  lcmineqlem6  42007  lcmineqlem11  42012  lcmineqlem18  42019  aks4d1p1p2  42043  aks4d1p1p6  42046  aks4d1p1p7  42047  aks4d1p1p5  42048  posbezout  42073  2np3bcnp1  42117  2ap1caineq  42118  sticksstones12a  42130  bcle2d  42152  mvrrsubd  42247  lsubrotld  42250  oddnumth  42284  sumcubes  42286  cxp112d  42314  cxp111d  42315  sn-negex12  42390  sn-addrid  42394  sn-subeu  42400  sn-0tie0  42424  zaddcomlem  42436  zaddcom  42437  cnreeu  42463  dffltz  42607  cu3addd  42654  3cubeslem2  42658  3cubeslem3l  42659  3cubeslem3r  42660  3cubeslem4  42662  pellexlem2  42803  pellexlem6  42807  pell1234qrreccl  42827  pell1234qrmulcl  42828  pell14qrdich  42842  rmxyneg  42893  rmxyadd  42894  jm2.19lem4  42965  jm2.26lem3  42974  sqrtcval  43614  int-rightdistd  44153  binomcxplemnn0  44322  binomcxplemrat  44323  binomcxplemfrat  44324  binomcxplemdvbinom  44326  binomcxplemnotnn0  44329  sub2times  45255  clim1fr1  45582  limcperiod  45609  addlimc  45629  coseq0  45845  fprodaddrecnncnvlem  45890  dvxpaek  45921  dvnxpaek  45923  dvnmul  45924  itgiccshift  45961  itgperiod  45962  stoweidlem1  45982  stoweidlem11  45992  stoweidlem13  45994  wallispilem4  46049  wallispilem5  46050  wallispi  46051  wallispi2lem1  46052  wallispi2lem2  46053  wallispi2  46054  stirlinglem1  46055  stirlinglem3  46057  stirlinglem4  46058  stirlinglem5  46059  stirlinglem6  46060  stirlinglem7  46061  stirlinglem10  46064  stirlinglem11  46065  stirlinglem12  46066  stirlinglem13  46067  stirlinglem15  46069  dirkerper  46077  dirkertrigeqlem1  46079  dirkertrigeqlem2  46080  dirkertrigeqlem3  46081  dirkeritg  46083  dirkercncflem2  46085  dirkercncflem4  46087  fourierdlem18  46106  fourierdlem26  46114  fourierdlem30  46118  fourierdlem48  46135  fourierdlem49  46136  fourierdlem79  46166  fourierdlem83  46170  fourierdlem92  46179  fourierdlem93  46180  fourierdlem103  46190  fourierdlem104  46191  fourierdlem111  46198  fourierdlem112  46199  smfmullem1  46772  sigaraf  46834  sigaras  46836  readdcnnred  47287  fldivmod  47322  fmtnorec4  47533  quad1  47604  requad01  47605  requad2  47607  gpgedgvtx1  48046  dignn0flhalflem1  48600  affinecomb2  48688  eenglngeehlnmlem1  48722  itschlc0yqe  48745  itsclc0yqsollem1  48747  itsclc0yqsol  48749  itscnhlc0xyqsol  48750  itsclc0xyqsolr  48754  2itscplem3  48765  itscnhlinecirc02plem1  48767  inlinecirc02plem  48771  sinhpcosh  49725