Theorem addcld 11164

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   + caddc 11041

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

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

This theorem is referenced by:  cnegex  11327  addcom  11332  addcomd  11348  muladd11r  11359  negeu  11383  addsubass  11403  subsub2  11422  subsub4  11427  pnncan  11435  addsub4  11437  addsubsub23  11558  pnpncand  11571  addmulsub  11612  subaddmulsub  11613  mulsubaddmulsub  11614  divdir  11834  cju  12155  cnref1o  12935  xov1plusxeqvd  13451  modaddb  13868  expaddz  14068  binom3  14186  sqoddm1div8  14205  mulsubdivbinom2  14224  muldivbinom2  14225  spllen  14716  crre  15076  remullem  15090  imval2  15113  cjreim2  15123  sqreulem  15322  bhmafibid1cn  15428  bhmafibid2cn  15429  bhmafibid1  15430  bhmafibid2  15431  addcn2  15556  o1add  15576  rlimadd  15605  fsumadd  15702  isumadd  15729  binomlem  15794  binomfallfaclem2  16005  bpoly4  16024  fsumcube  16025  efaddlem  16058  ef4p  16080  cosf  16092  tanval2  16100  tanval3  16101  resin4p  16105  recos4p  16106  efival  16119  sinadd  16131  cosadd  16132  tanadd  16134  pwp1fsum  16360  sadadd2lem2  16419  sadadd2lem  16428  pythagtriplem1  16787  pythagtriplem12  16797  pythagtriplem17  16802  pcbc  16871  mul4sqlem  16924  4sqlem14  16929  vdwlem6  16957  vdwlem9  16960  mulgdirlem  19081  blcvx  24763  cphpyth  25183  tcphcphlem1  25202  cphipval2  25208  4cphipval2  25209  csbren  25366  ovollb2lem  25455  mbfadd  25628  itgcnlem  25757  itgaddlem2  25791  dvmptre  25936  dvsincos  25948  itgpowd  26017  taylthlem2  26339  ptolemy  26460  tanregt0  26503  eff1olem  26512  cosargd  26572  tanarg  26583  logf1o2  26614  efopn  26622  cxpsqrtlem  26666  cxpeq  26721  ang180lem1  26773  ang180lem2  26774  ang180lem3  26775  ang180lem4  26776  pythag  26781  ssscongptld  26786  chordthmlem  26796  chordthmlem2  26797  chordthmlem3  26798  chordthmlem4  26799  chordthmlem5  26800  heron  26802  quad2  26803  dcubic1lem  26807  dcubic2  26808  dcubic1  26809  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  binom4  26814  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  quartlem2  26822  quartlem3  26823  quartlem4  26824  quart  26825  asinlem3  26835  asinf  26836  asinneg  26850  efiasin  26852  asinsinlem  26855  asinsin  26856  asinbnd  26863  atanlogaddlem  26877  dmgmaddnn0  26990  dmgmdivn0  26991  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamgulm2  26999  lgambdd  27000  lgamucov  27001  lgamcvg2  27018  gamcvg  27019  gamcvg2lem  27022  ftalem7  27042  basellem3  27046  bposlem9  27255  lgsquad2lem1  27347  2lgslem3d1  27366  2sqmod  27399  dchrvmasumiflem2  27465  mulogsumlem  27494  mulog2sumlem1  27497  mulog2sumlem2  27498  mulog2sumlem3  27499  selberglem1  27508  selberg2  27514  selberg3lem1  27520  selbergr  27531  selberg3r  27532  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntrlog2bnd  27547  brbtwn2  28974  colinearalglem1  28975  colinearalglem2  28976  axeuclidlem  29031  axcontlem2  29034  axcontlem7  29039  axcontlem8  29040  finsumvtxdg2ssteplem4  29617  wwlksext2clwwlk  30127  4ipval2  30779  dipcj  30785  golem1  32342  submuladdd  32813  binom2subadd  32814  pythagreim  32818  quad3d  32822  lt2addrd  32823  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2  33194  archirngz  33250  archiabllem2c  33256  zringfrac  33614  ccfldextdgrr  33816  constrrtll  33875  constrrtlc1  33876  constrrtcclem  33878  constrrtcc  33879  constrfin  33890  nn0constr  33905  constraddcl  33906  constrrecl  33913  constrresqrtcl  33921  constrsqrtcl  33923  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpiminply  33932  cos9thpinconstrlem1  33933  cos9thpinconstrlem2  33934  cnre2csqima  34055  ballotlemsima  34660  hgt750lemb  34800  iprodgam  35924  dnizphlfeqhlf  36736  dnibndlem9  36746  knoppndvlem16  36787  qdiff  37641  itg2addnclem3  37994  itgaddnclem2  38000  itgaddnc  38001  ftc1anclem6  38019  ftc1anclem8  38021  dvasin  38025  areacirclem1  38029  areacirclem4  38032  areacirc  38034  lcmineqlem6  42473  lcmineqlem11  42478  lcmineqlem18  42485  aks4d1p1p2  42509  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  posbezout  42539  2np3bcnp1  42583  2ap1caineq  42584  sticksstones12a  42596  bcle2d  42618  mvrrsubd  42706  lsubrotld  42709  oddnumth  42743  sumcubes  42745  cxp112d  42773  cxp111d  42774  sn-negex12  42849  sn-addrid  42853  sn-subeu  42859  sn-0tie0  42896  zaddcomlem  42908  zaddcom  42909  cnreeu  42935  dffltz  43067  cu3addd  43113  3cubeslem2  43117  3cubeslem3l  43118  3cubeslem3r  43119  3cubeslem4  43121  pellexlem2  43258  pellexlem6  43262  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell14qrdich  43297  rmxyneg  43348  rmxyadd  43349  jm2.19lem4  43420  jm2.26lem3  43429  sqrtcval  44068  int-rightdistd  44607  binomcxplemnn0  44776  binomcxplemrat  44777  binomcxplemfrat  44778  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  sub2times  45706  clim1fr1  46031  limcperiod  46058  addlimc  46076  coseq0  46292  fprodaddrecnncnvlem  46337  dvxpaek  46368  dvnxpaek  46370  dvnmul  46371  itgiccshift  46408  itgperiod  46409  stoweidlem1  46429  stoweidlem11  46439  stoweidlem13  46441  wallispilem4  46496  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem1  46502  stirlinglem3  46504  stirlinglem4  46505  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem10  46511  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  stirlinglem15  46516  dirkerper  46524  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkeritg  46530  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem18  46553  fourierdlem26  46561  fourierdlem30  46565  fourierdlem48  46582  fourierdlem49  46583  fourierdlem79  46613  fourierdlem83  46617  fourierdlem92  46626  fourierdlem93  46627  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  smfmullem1  47219  sigaraf  47281  sigaras  47283  sin5tlem1  47321  sin5tlem4  47324  sin5tlem5  47325  readdcnnred  47751  fldivmod  47792  fmtnorec4  48012  quad1  48096  requad01  48097  requad2  48099  gpgedgvtx1  48538  dignn0flhalflem1  49091  affinecomb2  49179  eenglngeehlnmlem1  49213  itschlc0yqe  49236  itsclc0yqsollem1  49238  itsclc0yqsol  49240  itscnhlc0xyqsol  49241  itsclc0xyqsolr  49245  2itscplem3  49256  itscnhlinecirc02plem1  49258  inlinecirc02plem  49262  sinhpcosh  50215