Theorem addcld 9938

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

Syntax hints:   → wi 4   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818

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

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  cnegex  10096  addcom  10101  addcomd  10117  muladd11r  10128  negeu  10150  addsubass  10170  subsub2  10188  subsub4  10193  pnpcan  10199  pnncan  10201  addsub4  10203  pnpncand  10331  divdir  10589  cju  10893  cnref1o  11703  xov1plusxeqvd  12189  expaddz  12766  binom3  12847  sqoddm1div8  12890  mulsubdivbinom2  12908  muldivbinom2  12909  spllen  13356  crre  13702  remullem  13716  imval2  13739  cjreim2  13749  sqreulem  13947  addcn2  14172  o1add  14192  fsumadd  14317  isumadd  14340  binomlem  14400  binomfallfaclem2  14610  bpoly4  14629  fsumcube  14630  efaddlem  14662  ef4p  14682  cosf  14694  tanval2  14702  tanval3  14703  resin4p  14707  recos4p  14708  efival  14721  sinadd  14733  cosadd  14734  tanadd  14736  pwp1fsum  14952  sadadd2lem2  15010  sadadd2lem  15019  pythagtriplem1  15359  pythagtriplem12  15369  pythagtriplem17  15374  pcbc  15442  mul4sqlem  15495  4sqlem14  15500  vdwlem6  15528  vdwlem9  15531  mulgdirlem  17395  blcvx  22409  tchcphlem1  22842  cphipval2  22848  4cphipval2  22849  csbren  22990  ovollb2lem  23063  mbfadd  23234  itgcnlem  23362  itgaddlem2  23396  dvmptre  23538  dvsincos  23548  taylthlem2  23932  ptolemy  24052  tanregt0  24089  eff1olem  24098  cosargd  24158  tanarg  24169  logf1o2  24196  efopn  24204  cxpsqrtlem  24248  cxpeq  24298  ang180lem1  24339  ang180lem2  24340  ang180lem3  24341  ang180lem4  24342  pythag  24347  ssscongptld  24352  chordthmlem  24359  chordthmlem2  24360  chordthmlem3  24361  chordthmlem4  24362  chordthmlem5  24363  heron  24365  quad2  24366  dcubic1lem  24370  dcubic2  24371  dcubic1  24372  dcubic  24373  mcubic  24374  cubic2  24375  cubic  24376  binom4  24377  dquartlem1  24378  dquartlem2  24379  dquart  24380  quart1cl  24381  quart1lem  24382  quart1  24383  quartlem1  24384  quartlem2  24385  quartlem3  24386  quartlem4  24387  quart  24388  asinlem3  24398  asinf  24399  asinneg  24413  efiasin  24415  asinsinlem  24418  asinsin  24419  asinbnd  24426  atanlogaddlem  24440  dmgmaddnn0  24553  dmgmdivn0  24554  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgambdd  24563  lgamucov  24564  lgamcvg2  24581  gamcvg  24582  gamcvg2lem  24585  ftalem7  24605  basellem3  24609  bposlem9  24817  lgsquad2lem1  24909  2lgslem3d1  24928  dchrvmasumiflem2  24991  mulogsumlem  25020  mulog2sumlem1  25023  mulog2sumlem2  25024  mulog2sumlem3  25025  selberglem1  25034  selberg2  25040  selberg3lem1  25046  selbergr  25057  selberg3r  25058  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntrlog2bnd  25073  brbtwn2  25585  colinearalglem1  25586  colinearalglem2  25587  axeuclidlem  25642  axcontlem2  25645  axcontlem7  25650  axcontlem8  25651  4ipval2  26947  dipcj  26953  golem1  28514  lt2addrd  28903  bhmafibid1  28975  bhmafibid2  28976  2sqmod  28979  archirngz  29074  archiabllem2c  29080  cnre2csqima  29285  ballotlemsima  29904  iprodgam  30881  dnizphlfeqhlf  31636  dnibndlem9  31646  knoppndvlem16  31688  itg2addnclem3  32633  itgaddnclem2  32639  itgaddnc  32640  ftc1anclem6  32660  ftc1anclem8  32662  dvasin  32666  areacirclem1  32670  areacirclem4  32673  areacirc  32675  pellexlem2  36412  pellexlem6  36416  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell14qrdich  36451  rmxyneg  36503  rmxyadd  36504  jm2.19lem4  36577  jm2.26lem3  36586  itgpowd  36819  int-rightdistd  37505  binomcxplemnn0  37570  binomcxplemrat  37571  binomcxplemfrat  37572  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  sub2times  38426  clim1fr1  38668  limcperiod  38695  addlimc  38715  coseq0  38747  fprodaddrecnncnvlem  38796  dvxpaek  38830  dvnxpaek  38832  dvnmul  38833  itgiccshift  38872  itgperiod  38873  stoweidlem1  38894  stoweidlem11  38904  stoweidlem13  38906  wallispilem4  38961  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  wallispi2  38966  stirlinglem1  38967  stirlinglem3  38969  stirlinglem4  38970  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem15  38981  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkeritg  38995  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem18  39018  fourierdlem26  39026  fourierdlem30  39030  fourierdlem48  39047  fourierdlem49  39048  fourierdlem79  39078  fourierdlem83  39082  fourierdlem92  39091  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  smfmullem1  39676  sigaraf  39691  sigaras  39693  fmtnorec4  39999  fldivmod  42107  dignn0flhalflem1  42207  sinhpcosh  42280