Theorem addcld 11163

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 7368  ℂ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  11326  addcom  11331  addcomd  11347  muladd11r  11358  negeu  11382  addsubass  11402  subsub2  11421  subsub4  11426  pnncan  11434  addsub4  11436  addsubsub23  11557  pnpncand  11570  addmulsub  11611  subaddmulsub  11612  mulsubaddmulsub  11613  divdir  11833  cju  12153  cnref1o  12910  xov1plusxeqvd  13426  modaddb  13841  expaddz  14041  binom3  14159  sqoddm1div8  14178  mulsubdivbinom2  14197  muldivbinom2  14198  spllen  14689  crre  15049  remullem  15063  imval2  15086  cjreim2  15096  sqreulem  15295  bhmafibid1cn  15401  bhmafibid2cn  15402  bhmafibid1  15403  bhmafibid2  15404  addcn2  15529  o1add  15549  rlimadd  15578  fsumadd  15675  isumadd  15702  binomlem  15764  binomfallfaclem2  15975  bpoly4  15994  fsumcube  15995  efaddlem  16028  ef4p  16050  cosf  16062  tanval2  16070  tanval3  16071  resin4p  16075  recos4p  16076  efival  16089  sinadd  16101  cosadd  16102  tanadd  16104  pwp1fsum  16330  sadadd2lem2  16389  sadadd2lem  16398  pythagtriplem1  16756  pythagtriplem12  16766  pythagtriplem17  16771  pcbc  16840  mul4sqlem  16893  4sqlem14  16898  vdwlem6  16926  vdwlem9  16929  mulgdirlem  19047  blcvx  24754  cphpyth  25184  tcphcphlem1  25203  cphipval2  25209  4cphipval2  25210  csbren  25367  ovollb2lem  25457  mbfadd  25630  itgcnlem  25759  itgaddlem2  25793  dvmptre  25941  dvsincos  25953  itgpowd  26025  taylthlem2  26350  taylthlem2OLD  26351  ptolemy  26473  tanregt0  26516  eff1olem  26525  cosargd  26585  tanarg  26596  logf1o2  26627  efopn  26635  cxpsqrtlem  26679  cxpeq  26735  ang180lem1  26787  ang180lem2  26788  ang180lem3  26789  ang180lem4  26790  pythag  26795  ssscongptld  26800  chordthmlem  26810  chordthmlem2  26811  chordthmlem3  26812  chordthmlem4  26813  chordthmlem5  26814  heron  26816  quad2  26817  dcubic1lem  26821  dcubic2  26822  dcubic1  26823  dcubic  26824  mcubic  26825  cubic2  26826  cubic  26827  binom4  26828  dquartlem1  26829  dquartlem2  26830  dquart  26831  quart1cl  26832  quart1lem  26833  quart1  26834  quartlem1  26835  quartlem2  26836  quartlem3  26837  quartlem4  26838  quart  26839  asinlem3  26849  asinf  26850  asinneg  26864  efiasin  26866  asinsinlem  26869  asinsin  26870  asinbnd  26877  atanlogaddlem  26891  dmgmaddnn0  27005  dmgmdivn0  27006  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem4  27010  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamgulm2  27014  lgambdd  27015  lgamucov  27016  lgamcvg2  27033  gamcvg  27034  gamcvg2lem  27037  ftalem7  27057  basellem3  27061  bposlem9  27271  lgsquad2lem1  27363  2lgslem3d1  27382  2sqmod  27415  dchrvmasumiflem2  27481  mulogsumlem  27510  mulog2sumlem1  27513  mulog2sumlem2  27514  mulog2sumlem3  27515  selberglem1  27524  selberg2  27530  selberg3lem1  27536  selbergr  27547  selberg3r  27548  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  brbtwn2  28990  colinearalglem1  28991  colinearalglem2  28992  axeuclidlem  29047  axcontlem2  29050  axcontlem7  29055  axcontlem8  29056  finsumvtxdg2ssteplem4  29634  wwlksext2clwwlk  30144  4ipval2  30796  dipcj  30802  golem1  32359  submuladdd  32830  binom2subadd  32832  pythagreim  32836  quad3d  32840  lt2addrd  32841  cycpmco2lem3  33222  cycpmco2lem4  33223  cycpmco2lem5  33224  cycpmco2lem6  33225  cycpmco2  33227  archirngz  33283  archiabllem2c  33289  zringfrac  33647  ccfldextdgrr  33850  constrrtll  33909  constrrtlc1  33910  constrrtcclem  33912  constrrtcc  33913  constrfin  33924  nn0constr  33939  constraddcl  33940  constrrecl  33947  constrresqrtcl  33955  constrsqrtcl  33957  cos9thpiminplylem1  33960  cos9thpiminplylem2  33961  cos9thpiminplylem3  33962  cos9thpiminply  33966  cos9thpinconstrlem1  33967  cos9thpinconstrlem2  33968  cnre2csqima  34089  ballotlemsima  34694  hgt750lemb  34834  iprodgam  35958  dnizphlfeqhlf  36698  dnibndlem9  36708  knoppndvlem16  36749  itg2addnclem3  37924  itgaddnclem2  37930  itgaddnc  37931  ftc1anclem6  37949  ftc1anclem8  37951  dvasin  37955  areacirclem1  37959  areacirclem4  37962  areacirc  37964  lcmineqlem6  42404  lcmineqlem11  42409  lcmineqlem18  42416  aks4d1p1p2  42440  aks4d1p1p6  42443  aks4d1p1p7  42444  aks4d1p1p5  42445  posbezout  42470  2np3bcnp1  42514  2ap1caineq  42515  sticksstones12a  42527  bcle2d  42549  mvrrsubd  42644  lsubrotld  42647  oddnumth  42681  sumcubes  42683  cxp112d  42711  cxp111d  42712  sn-negex12  42787  sn-addrid  42791  sn-subeu  42797  sn-0tie0  42821  zaddcomlem  42833  zaddcom  42834  cnreeu  42860  dffltz  42992  cu3addd  43038  3cubeslem2  43042  3cubeslem3l  43043  3cubeslem3r  43044  3cubeslem4  43046  pellexlem2  43187  pellexlem6  43191  pell1234qrreccl  43211  pell1234qrmulcl  43212  pell14qrdich  43226  rmxyneg  43277  rmxyadd  43278  jm2.19lem4  43349  jm2.26lem3  43358  sqrtcval  43997  int-rightdistd  44536  binomcxplemnn0  44705  binomcxplemrat  44706  binomcxplemfrat  44707  binomcxplemdvbinom  44709  binomcxplemnotnn0  44712  sub2times  45635  clim1fr1  45961  limcperiod  45988  addlimc  46006  coseq0  46222  fprodaddrecnncnvlem  46267  dvxpaek  46298  dvnxpaek  46300  dvnmul  46301  itgiccshift  46338  itgperiod  46339  stoweidlem1  46359  stoweidlem11  46369  stoweidlem13  46371  wallispilem4  46426  wallispilem5  46427  wallispi  46428  wallispi2lem1  46429  wallispi2lem2  46430  wallispi2  46431  stirlinglem1  46432  stirlinglem3  46434  stirlinglem4  46435  stirlinglem5  46436  stirlinglem6  46437  stirlinglem7  46438  stirlinglem10  46441  stirlinglem11  46442  stirlinglem12  46443  stirlinglem13  46444  stirlinglem15  46446  dirkerper  46454  dirkertrigeqlem1  46456  dirkertrigeqlem2  46457  dirkertrigeqlem3  46458  dirkeritg  46460  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem18  46483  fourierdlem26  46491  fourierdlem30  46495  fourierdlem48  46512  fourierdlem49  46513  fourierdlem79  46543  fourierdlem83  46547  fourierdlem92  46556  fourierdlem93  46557  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  fourierdlem112  46576  smfmullem1  47149  sigaraf  47211  sigaras  47213  readdcnnred  47663  fldivmod  47698  fmtnorec4  47909  quad1  47980  requad01  47981  requad2  47983  gpgedgvtx1  48422  dignn0flhalflem1  48975  affinecomb2  49063  eenglngeehlnmlem1  49097  itschlc0yqe  49120  itsclc0yqsollem1  49122  itsclc0yqsol  49124  itscnhlc0xyqsol  49125  itsclc0xyqsolr  49129  2itscplem3  49140  itscnhlinecirc02plem1  49142  inlinecirc02plem  49146  sinhpcosh  50099