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  28194  colinearalglem1  28195  colinearalglem2  28196  axeuclidlem  28251  axcontlem2  28254  axcontlem7  28259  axcontlem8  28260  finsumvtxdg2ssteplem4  28836  wwlksext2clwwlk  29341  4ipval2  29992  dipcj  29998  golem1  31555  lt2addrd  31995  cycpmco2lem3  32318  cycpmco2lem4  32319  cycpmco2lem5  32320  cycpmco2lem6  32321  cycpmco2  32323  archirngz  32366  archiabllem2c  32372  ccfldextdgrr  32777  cnre2csqima  32922  ballotlemsima  33545  hgt750lemb  33699  iprodgam  34743  gg-cncrng  35231  dnizphlfeqhlf  35400  dnibndlem9  35410  knoppndvlem16  35451  itg2addnclem3  36589  itgaddnclem2  36595  itgaddnc  36596  ftc1anclem6  36614  ftc1anclem8  36616  dvasin  36620  areacirclem1  36624  areacirclem4  36627  areacirc  36629  lcmineqlem6  40947  lcmineqlem11  40952  lcmineqlem18  40959  aks4d1p1p2  40983  aks4d1p1p6  40986  aks4d1p1p7  40987  aks4d1p1p5  40988  2np3bcnp1  41008  2ap1caineq  41009  sticksstones12a  41021  metakunt29  41061  mvrrsubd  41235  lsubrotld  41238  oddnumth  41257  sumcubes  41259  sn-negex12  41337  sn-addrid  41341  sn-subeu  41347  sn-0tie0  41360  zaddcomlem  41372  zaddcom  41373  cnreeu  41389  dffltz  41424  cu3addd  41466  3cubeslem2  41471  3cubeslem3l  41472  3cubeslem3r  41473  3cubeslem4  41475  pellexlem2  41616  pellexlem6  41620  pell1234qrreccl  41640  pell1234qrmulcl  41641  pell14qrdich  41655  rmxyneg  41707  rmxyadd  41708  jm2.19lem4  41779  jm2.26lem3  41788  sqrtcval  42440  int-rightdistd  42980  binomcxplemnn0  43156  binomcxplemrat  43157  binomcxplemfrat  43158  binomcxplemdvbinom  43160  binomcxplemnotnn0  43163  sub2times  44030  clim1fr1  44365  limcperiod  44392  addlimc  44412  coseq0  44628  fprodaddrecnncnvlem  44673  dvxpaek  44704  dvnxpaek  44706  dvnmul  44707  itgiccshift  44744  itgperiod  44745  stoweidlem1  44765  stoweidlem11  44775  stoweidlem13  44777  wallispilem4  44832  wallispilem5  44833  wallispi  44834  wallispi2lem1  44835  wallispi2lem2  44836  wallispi2  44837  stirlinglem1  44838  stirlinglem3  44840  stirlinglem4  44841  stirlinglem5  44842  stirlinglem6  44843  stirlinglem7  44844  stirlinglem10  44847  stirlinglem11  44848  stirlinglem12  44849  stirlinglem13  44850  stirlinglem15  44852  dirkerper  44860  dirkertrigeqlem1  44862  dirkertrigeqlem2  44863  dirkertrigeqlem3  44864  dirkeritg  44866  dirkercncflem2  44868  dirkercncflem4  44870  fourierdlem18  44889  fourierdlem26  44897  fourierdlem30  44901  fourierdlem48  44918  fourierdlem49  44919  fourierdlem79  44949  fourierdlem83  44953  fourierdlem92  44962  fourierdlem93  44963  fourierdlem103  44973  fourierdlem104  44974  fourierdlem111  44981  fourierdlem112  44982  smfmullem1  45555  sigaraf  45617  sigaras  45619  readdcnnred  46059  fmtnorec4  46265  quad1  46336  requad01  46337  requad2  46339  fldivmod  47252  dignn0flhalflem1  47349  affinecomb2  47437  eenglngeehlnmlem1  47471  itschlc0yqe  47494  itsclc0yqsollem1  47496  itsclc0yqsol  47498  itscnhlc0xyqsol  47499  itsclc0xyqsolr  47503  2itscplem3  47514  itscnhlinecirc02plem1  47516  inlinecirc02plem  47520  sinhpcosh  47833