Theorem addcld 11233

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   + caddc 11113

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

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  cnegex  11395  addcom  11400  addcomd  11416  muladd11r  11427  negeu  11450  addsubass  11470  subsub2  11488  subsub4  11493  pnncan  11501  addsub4  11503  pnpncand  11635  addmulsub  11676  subaddmulsub  11677  mulsubaddmulsub  11678  divdir  11897  cju  12208  cnref1o  12969  xov1plusxeqvd  13475  expaddz  14072  binom3  14187  sqoddm1div8  14206  mulsubdivbinom2  14222  muldivbinom2  14223  spllen  14704  crre  15061  remullem  15075  imval2  15098  cjreim2  15108  sqreulem  15306  bhmafibid1cn  15410  bhmafibid2cn  15411  bhmafibid1  15412  bhmafibid2  15413  addcn2  15538  o1add  15558  rlimadd  15587  fsumadd  15686  isumadd  15713  binomlem  15775  binomfallfaclem2  15984  bpoly4  16003  fsumcube  16004  efaddlem  16036  ef4p  16056  cosf  16068  tanval2  16076  tanval3  16077  resin4p  16081  recos4p  16082  efival  16095  sinadd  16107  cosadd  16108  tanadd  16110  pwp1fsum  16334  sadadd2lem2  16391  sadadd2lem  16400  pythagtriplem1  16749  pythagtriplem12  16759  pythagtriplem17  16764  pcbc  16833  mul4sqlem  16886  4sqlem14  16891  vdwlem6  16919  vdwlem9  16922  mulgdirlem  18985  blcvx  24314  cphpyth  24733  tcphcphlem1  24752  cphipval2  24758  4cphipval2  24759  csbren  24916  ovollb2lem  25005  mbfadd  25178  itgcnlem  25307  itgaddlem2  25341  dvmptre  25486  dvsincos  25498  itgpowd  25567  taylthlem2  25886  ptolemy  26006  tanregt0  26048  eff1olem  26057  cosargd  26116  tanarg  26127  logf1o2  26158  efopn  26166  cxpsqrtlem  26210  cxpeq  26265  ang180lem1  26314  ang180lem2  26315  ang180lem3  26316  ang180lem4  26317  pythag  26322  ssscongptld  26327  chordthmlem  26337  chordthmlem2  26338  chordthmlem3  26339  chordthmlem4  26340  chordthmlem5  26341  heron  26343  quad2  26344  dcubic1lem  26348  dcubic2  26349  dcubic1  26350  dcubic  26351  mcubic  26352  cubic2  26353  cubic  26354  binom4  26355  dquartlem1  26356  dquartlem2  26357  dquart  26358  quart1cl  26359  quart1lem  26360  quart1  26361  quartlem1  26362  quartlem2  26363  quartlem3  26364  quartlem4  26365  quart  26366  asinlem3  26376  asinf  26377  asinneg  26391  efiasin  26393  asinsinlem  26396  asinsin  26397  asinbnd  26404  atanlogaddlem  26418  dmgmaddnn0  26531  dmgmdivn0  26532  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem4  26536  lgamgulmlem5  26537  lgamgulmlem6  26538  lgamgulm2  26540  lgambdd  26541  lgamucov  26542  lgamcvg2  26559  gamcvg  26560  gamcvg2lem  26563  ftalem7  26583  basellem3  26587  bposlem9  26795  lgsquad2lem1  26887  2lgslem3d1  26906  2sqmod  26939  dchrvmasumiflem2  27005  mulogsumlem  27034  mulog2sumlem1  27037  mulog2sumlem2  27038  mulog2sumlem3  27039  selberglem1  27048  selberg2  27054  selberg3lem1  27060  selbergr  27071  selberg3r  27072  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntrlog2bnd  27087  brbtwn2  28163  colinearalglem1  28164  colinearalglem2  28165  axeuclidlem  28220  axcontlem2  28223  axcontlem7  28228  axcontlem8  28229  finsumvtxdg2ssteplem4  28805  wwlksext2clwwlk  29310  4ipval2  29961  dipcj  29967  golem1  31524  lt2addrd  31964  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2  32292  archirngz  32335  archiabllem2c  32341  ccfldextdgrr  32746  cnre2csqima  32891  ballotlemsima  33514  hgt750lemb  33668  iprodgam  34712  dnizphlfeqhlf  35352  dnibndlem9  35362  knoppndvlem16  35403  itg2addnclem3  36541  itgaddnclem2  36547  itgaddnc  36548  ftc1anclem6  36566  ftc1anclem8  36568  dvasin  36572  areacirclem1  36576  areacirclem4  36579  areacirc  36581  lcmineqlem6  40899  lcmineqlem11  40904  lcmineqlem18  40911  aks4d1p1p2  40935  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  2np3bcnp1  40960  2ap1caineq  40961  sticksstones12a  40973  metakunt29  41013  mvrrsubd  41187  lsubrotld  41190  oddnumth  41209  sumcubes  41211  sn-negex12  41289  sn-addrid  41293  sn-subeu  41299  sn-0tie0  41312  zaddcomlem  41324  zaddcom  41325  cnreeu  41341  dffltz  41376  cu3addd  41418  3cubeslem2  41423  3cubeslem3l  41424  3cubeslem3r  41425  3cubeslem4  41427  pellexlem2  41568  pellexlem6  41572  pell1234qrreccl  41592  pell1234qrmulcl  41593  pell14qrdich  41607  rmxyneg  41659  rmxyadd  41660  jm2.19lem4  41731  jm2.26lem3  41740  sqrtcval  42392  int-rightdistd  42932  binomcxplemnn0  43108  binomcxplemrat  43109  binomcxplemfrat  43110  binomcxplemdvbinom  43112  binomcxplemnotnn0  43115  sub2times  43982  clim1fr1  44317  limcperiod  44344  addlimc  44364  coseq0  44580  fprodaddrecnncnvlem  44625  dvxpaek  44656  dvnxpaek  44658  dvnmul  44659  itgiccshift  44696  itgperiod  44697  stoweidlem1  44717  stoweidlem11  44727  stoweidlem13  44729  wallispilem4  44784  wallispilem5  44785  wallispi  44786  wallispi2lem1  44787  wallispi2lem2  44788  wallispi2  44789  stirlinglem1  44790  stirlinglem3  44792  stirlinglem4  44793  stirlinglem5  44794  stirlinglem6  44795  stirlinglem7  44796  stirlinglem10  44799  stirlinglem11  44800  stirlinglem12  44801  stirlinglem13  44802  stirlinglem15  44804  dirkerper  44812  dirkertrigeqlem1  44814  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  dirkeritg  44818  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem18  44841  fourierdlem26  44849  fourierdlem30  44853  fourierdlem48  44870  fourierdlem49  44871  fourierdlem79  44901  fourierdlem83  44905  fourierdlem92  44914  fourierdlem93  44915  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fourierdlem112  44934  smfmullem1  45507  sigaraf  45569  sigaras  45571  readdcnnred  46011  fmtnorec4  46217  quad1  46288  requad01  46289  requad2  46291  fldivmod  47204  dignn0flhalflem1  47301  affinecomb2  47389  eenglngeehlnmlem1  47423  itschlc0yqe  47446  itsclc0yqsollem1  47448  itsclc0yqsol  47450  itscnhlc0xyqsol  47451  itsclc0xyqsolr  47455  2itscplem3  47466  itscnhlinecirc02plem1  47468  inlinecirc02plem  47472  sinhpcosh  47785