Theorem addcld 11193

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071

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

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

This theorem is referenced by:  cnegex  11355  addcom  11360  addcomd  11376  muladd11r  11387  negeu  11411  addsubass  11431  subsub2  11450  subsub4  11455  pnncan  11463  addsub4  11465  addsubsub23  11586  pnpncand  11599  addmulsub  11640  subaddmulsub  11641  mulsubaddmulsub  11642  divdir  11862  cju  12182  cnref1o  12944  xov1plusxeqvd  13459  modaddb  13871  expaddz  14071  binom3  14189  sqoddm1div8  14208  mulsubdivbinom2  14227  muldivbinom2  14228  spllen  14719  crre  15080  remullem  15094  imval2  15117  cjreim2  15127  sqreulem  15326  bhmafibid1cn  15432  bhmafibid2cn  15433  bhmafibid1  15434  bhmafibid2  15435  addcn2  15560  o1add  15580  rlimadd  15609  fsumadd  15706  isumadd  15733  binomlem  15795  binomfallfaclem2  16006  bpoly4  16025  fsumcube  16026  efaddlem  16059  ef4p  16081  cosf  16093  tanval2  16101  tanval3  16102  resin4p  16106  recos4p  16107  efival  16120  sinadd  16132  cosadd  16133  tanadd  16135  pwp1fsum  16361  sadadd2lem2  16420  sadadd2lem  16429  pythagtriplem1  16787  pythagtriplem12  16797  pythagtriplem17  16802  pcbc  16871  mul4sqlem  16924  4sqlem14  16929  vdwlem6  16957  vdwlem9  16960  mulgdirlem  19037  blcvx  24686  cphpyth  25116  tcphcphlem1  25135  cphipval2  25141  4cphipval2  25142  csbren  25299  ovollb2lem  25389  mbfadd  25562  itgcnlem  25691  itgaddlem2  25725  dvmptre  25873  dvsincos  25885  itgpowd  25957  taylthlem2  26282  taylthlem2OLD  26283  ptolemy  26405  tanregt0  26448  eff1olem  26457  cosargd  26517  tanarg  26528  logf1o2  26559  efopn  26567  cxpsqrtlem  26611  cxpeq  26667  ang180lem1  26719  ang180lem2  26720  ang180lem3  26721  ang180lem4  26722  pythag  26727  ssscongptld  26732  chordthmlem  26742  chordthmlem2  26743  chordthmlem3  26744  chordthmlem4  26745  chordthmlem5  26746  heron  26748  quad2  26749  dcubic1lem  26753  dcubic2  26754  dcubic1  26755  dcubic  26756  mcubic  26757  cubic2  26758  cubic  26759  binom4  26760  dquartlem1  26761  dquartlem2  26762  dquart  26763  quart1cl  26764  quart1lem  26765  quart1  26766  quartlem1  26767  quartlem2  26768  quartlem3  26769  quartlem4  26770  quart  26771  asinlem3  26781  asinf  26782  asinneg  26796  efiasin  26798  asinsinlem  26801  asinsin  26802  asinbnd  26809  atanlogaddlem  26823  dmgmaddnn0  26937  dmgmdivn0  26938  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem4  26942  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamgulm2  26946  lgambdd  26947  lgamucov  26948  lgamcvg2  26965  gamcvg  26966  gamcvg2lem  26969  ftalem7  26989  basellem3  26993  bposlem9  27203  lgsquad2lem1  27295  2lgslem3d1  27314  2sqmod  27347  dchrvmasumiflem2  27413  mulogsumlem  27442  mulog2sumlem1  27445  mulog2sumlem2  27446  mulog2sumlem3  27447  selberglem1  27456  selberg2  27462  selberg3lem1  27468  selbergr  27479  selberg3r  27480  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  brbtwn2  28832  colinearalglem1  28833  colinearalglem2  28834  axeuclidlem  28889  axcontlem2  28892  axcontlem7  28897  axcontlem8  28898  finsumvtxdg2ssteplem4  29476  wwlksext2clwwlk  29986  4ipval2  30637  dipcj  30643  golem1  32200  submuladdd  32663  binom2subadd  32665  pythagreim  32669  quad3d  32673  lt2addrd  32674  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  archirngz  33143  archiabllem2c  33149  zringfrac  33525  ccfldextdgrr  33667  constrrtll  33721  constrrtlc1  33722  constrrtcclem  33724  constrrtcc  33725  constrfin  33736  nn0constr  33751  constraddcl  33752  constrrecl  33759  constrresqrtcl  33767  constrsqrtcl  33769  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpiminply  33778  cos9thpinconstrlem1  33779  cos9thpinconstrlem2  33780  cnre2csqima  33901  ballotlemsima  34507  hgt750lemb  34647  iprodgam  35729  dnizphlfeqhlf  36464  dnibndlem9  36474  knoppndvlem16  36515  itg2addnclem3  37667  itgaddnclem2  37673  itgaddnc  37674  ftc1anclem6  37692  ftc1anclem8  37694  dvasin  37698  areacirclem1  37702  areacirclem4  37705  areacirc  37707  lcmineqlem6  42022  lcmineqlem11  42027  lcmineqlem18  42034  aks4d1p1p2  42058  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  posbezout  42088  2np3bcnp1  42132  2ap1caineq  42133  sticksstones12a  42145  bcle2d  42167  mvrrsubd  42262  lsubrotld  42265  oddnumth  42299  sumcubes  42301  cxp112d  42329  cxp111d  42330  sn-negex12  42405  sn-addrid  42409  sn-subeu  42415  sn-0tie0  42439  zaddcomlem  42451  zaddcom  42452  cnreeu  42478  dffltz  42622  cu3addd  42669  3cubeslem2  42673  3cubeslem3l  42674  3cubeslem3r  42675  3cubeslem4  42677  pellexlem2  42818  pellexlem6  42822  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell14qrdich  42857  rmxyneg  42909  rmxyadd  42910  jm2.19lem4  42981  jm2.26lem3  42990  sqrtcval  43630  int-rightdistd  44169  binomcxplemnn0  44338  binomcxplemrat  44339  binomcxplemfrat  44340  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  sub2times  45271  clim1fr1  45599  limcperiod  45626  addlimc  45646  coseq0  45862  fprodaddrecnncnvlem  45907  dvxpaek  45938  dvnxpaek  45940  dvnmul  45941  itgiccshift  45978  itgperiod  45979  stoweidlem1  45999  stoweidlem11  46009  stoweidlem13  46011  wallispilem4  46066  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem15  46086  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkeritg  46100  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem18  46123  fourierdlem26  46131  fourierdlem30  46135  fourierdlem48  46152  fourierdlem49  46153  fourierdlem79  46183  fourierdlem83  46187  fourierdlem92  46196  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  smfmullem1  46789  sigaraf  46851  sigaras  46853  readdcnnred  47304  fldivmod  47339  fmtnorec4  47550  quad1  47621  requad01  47622  requad2  47624  gpgedgvtx1  48053  dignn0flhalflem1  48604  affinecomb2  48692  eenglngeehlnmlem1  48726  itschlc0yqe  48749  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itsclc0xyqsolr  48758  2itscplem3  48769  itscnhlinecirc02plem1  48771  inlinecirc02plem  48775  sinhpcosh  49729