Theorem addcld 11259

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132   + caddc 11137

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

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

This theorem is referenced by:  cnegex  11421  addcom  11426  addcomd  11442  muladd11r  11453  negeu  11477  addsubass  11497  subsub2  11516  subsub4  11521  pnncan  11529  addsub4  11531  pnpncand  11663  addmulsub  11704  subaddmulsub  11705  mulsubaddmulsub  11706  divdir  11926  cju  12241  cnref1o  13006  xov1plusxeqvd  13520  expaddz  14129  binom3  14247  sqoddm1div8  14266  mulsubdivbinom2  14285  muldivbinom2  14286  spllen  14777  crre  15138  remullem  15152  imval2  15175  cjreim2  15185  sqreulem  15383  bhmafibid1cn  15487  bhmafibid2cn  15488  bhmafibid1  15489  bhmafibid2  15490  addcn2  15615  o1add  15635  rlimadd  15664  fsumadd  15761  isumadd  15788  binomlem  15850  binomfallfaclem2  16061  bpoly4  16080  fsumcube  16081  efaddlem  16114  ef4p  16136  cosf  16148  tanval2  16156  tanval3  16157  resin4p  16161  recos4p  16162  efival  16175  sinadd  16187  cosadd  16188  tanadd  16190  pwp1fsum  16415  sadadd2lem2  16474  sadadd2lem  16483  pythagtriplem1  16841  pythagtriplem12  16851  pythagtriplem17  16856  pcbc  16925  mul4sqlem  16978  4sqlem14  16983  vdwlem6  17011  vdwlem9  17014  mulgdirlem  19093  blcvx  24742  cphpyth  25173  tcphcphlem1  25192  cphipval2  25198  4cphipval2  25199  csbren  25356  ovollb2lem  25446  mbfadd  25619  itgcnlem  25748  itgaddlem2  25782  dvmptre  25930  dvsincos  25942  itgpowd  26014  taylthlem2  26339  taylthlem2OLD  26340  ptolemy  26462  tanregt0  26505  eff1olem  26514  cosargd  26574  tanarg  26585  logf1o2  26616  efopn  26624  cxpsqrtlem  26668  cxpeq  26724  ang180lem1  26776  ang180lem2  26777  ang180lem3  26778  ang180lem4  26779  pythag  26784  ssscongptld  26789  chordthmlem  26799  chordthmlem2  26800  chordthmlem3  26801  chordthmlem4  26802  chordthmlem5  26803  heron  26805  quad2  26806  dcubic1lem  26810  dcubic2  26811  dcubic1  26812  dcubic  26813  mcubic  26814  cubic2  26815  cubic  26816  binom4  26817  dquartlem1  26818  dquartlem2  26819  dquart  26820  quart1cl  26821  quart1lem  26822  quart1  26823  quartlem1  26824  quartlem2  26825  quartlem3  26826  quartlem4  26827  quart  26828  asinlem3  26838  asinf  26839  asinneg  26853  efiasin  26855  asinsinlem  26858  asinsin  26859  asinbnd  26866  atanlogaddlem  26880  dmgmaddnn0  26994  dmgmdivn0  26995  lgamgulmlem2  26997  lgamgulmlem3  26998  lgamgulmlem4  26999  lgamgulmlem5  27000  lgamgulmlem6  27001  lgamgulm2  27003  lgambdd  27004  lgamucov  27005  lgamcvg2  27022  gamcvg  27023  gamcvg2lem  27026  ftalem7  27046  basellem3  27050  bposlem9  27260  lgsquad2lem1  27352  2lgslem3d1  27371  2sqmod  27404  dchrvmasumiflem2  27470  mulogsumlem  27499  mulog2sumlem1  27502  mulog2sumlem2  27503  mulog2sumlem3  27504  selberglem1  27513  selberg2  27519  selberg3lem1  27525  selbergr  27536  selberg3r  27537  pntrlog2bndlem1  27545  pntrlog2bndlem2  27546  pntrlog2bndlem5  27549  pntrlog2bndlem6  27551  pntrlog2bnd  27552  brbtwn2  28889  colinearalglem1  28890  colinearalglem2  28891  axeuclidlem  28946  axcontlem2  28949  axcontlem7  28954  axcontlem8  28955  finsumvtxdg2ssteplem4  29533  wwlksext2clwwlk  30043  4ipval2  30694  dipcj  30700  golem1  32257  submuladdd  32722  binom2subadd  32724  pythagreim  32728  quad3d  32732  lt2addrd  32733  cycpmco2lem3  33144  cycpmco2lem4  33145  cycpmco2lem5  33146  cycpmco2lem6  33147  cycpmco2  33149  archirngz  33192  archiabllem2c  33198  zringfrac  33574  ccfldextdgrr  33718  constrrtll  33770  constrrtlc1  33771  constrrtcclem  33773  constrrtcc  33774  constrfin  33785  nn0constr  33800  constraddcl  33801  constrrecl  33808  constrresqrtcl  33816  constrsqrtcl  33818  cos9thpiminplylem1  33821  cos9thpiminplylem2  33822  cos9thpiminplylem3  33823  cos9thpiminply  33827  cos9thpinconstrlem1  33828  cnre2csqima  33947  ballotlemsima  34553  hgt750lemb  34693  iprodgam  35764  dnizphlfeqhlf  36499  dnibndlem9  36509  knoppndvlem16  36550  itg2addnclem3  37702  itgaddnclem2  37708  itgaddnc  37709  ftc1anclem6  37727  ftc1anclem8  37729  dvasin  37733  areacirclem1  37737  areacirclem4  37740  areacirc  37742  lcmineqlem6  42052  lcmineqlem11  42057  lcmineqlem18  42064  aks4d1p1p2  42088  aks4d1p1p6  42091  aks4d1p1p7  42092  aks4d1p1p5  42093  posbezout  42118  2np3bcnp1  42162  2ap1caineq  42163  sticksstones12a  42175  bcle2d  42197  mvrrsubd  42292  lsubrotld  42295  oddnumth  42329  sumcubes  42331  cxp112d  42359  cxp111d  42360  sn-negex12  42434  sn-addrid  42438  sn-subeu  42444  sn-0tie0  42457  zaddcomlem  42469  zaddcom  42470  cnreeu  42488  dffltz  42632  cu3addd  42679  3cubeslem2  42683  3cubeslem3l  42684  3cubeslem3r  42685  3cubeslem4  42687  pellexlem2  42828  pellexlem6  42832  pell1234qrreccl  42852  pell1234qrmulcl  42853  pell14qrdich  42867  rmxyneg  42919  rmxyadd  42920  jm2.19lem4  42991  jm2.26lem3  43000  sqrtcval  43640  int-rightdistd  44179  binomcxplemnn0  44348  binomcxplemrat  44349  binomcxplemfrat  44350  binomcxplemdvbinom  44352  binomcxplemnotnn0  44355  sub2times  45281  clim1fr1  45610  limcperiod  45637  addlimc  45657  coseq0  45873  fprodaddrecnncnvlem  45918  dvxpaek  45949  dvnxpaek  45951  dvnmul  45952  itgiccshift  45989  itgperiod  45990  stoweidlem1  46010  stoweidlem11  46020  stoweidlem13  46022  wallispilem4  46077  wallispilem5  46078  wallispi  46079  wallispi2lem1  46080  wallispi2lem2  46081  wallispi2  46082  stirlinglem1  46083  stirlinglem3  46085  stirlinglem4  46086  stirlinglem5  46087  stirlinglem6  46088  stirlinglem7  46089  stirlinglem10  46092  stirlinglem11  46093  stirlinglem12  46094  stirlinglem13  46095  stirlinglem15  46097  dirkerper  46105  dirkertrigeqlem1  46107  dirkertrigeqlem2  46108  dirkertrigeqlem3  46109  dirkeritg  46111  dirkercncflem2  46113  dirkercncflem4  46115  fourierdlem18  46134  fourierdlem26  46142  fourierdlem30  46146  fourierdlem48  46163  fourierdlem49  46164  fourierdlem79  46194  fourierdlem83  46198  fourierdlem92  46207  fourierdlem93  46208  fourierdlem103  46218  fourierdlem104  46219  fourierdlem111  46226  fourierdlem112  46227  smfmullem1  46800  sigaraf  46862  sigaras  46864  readdcnnred  47312  fldivmod  47347  fmtnorec4  47543  quad1  47614  requad01  47615  requad2  47617  gpgedgvtx1  48046  dignn0flhalflem1  48575  affinecomb2  48663  eenglngeehlnmlem1  48697  itschlc0yqe  48720  itsclc0yqsollem1  48722  itsclc0yqsol  48724  itscnhlc0xyqsol  48725  itsclc0xyqsolr  48729  2itscplem3  48740  itscnhlinecirc02plem1  48742  inlinecirc02plem  48746  sinhpcosh  49584