Theorem addcld 9519

Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	|- ( ph -> A e. CC )
addcld.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
addcld	|- ( ph -> ( A + B ) e. CC )

Proof of Theorem addcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		addcld.2	. 2 |- ( ph -> B e. CC )
3		addcl 9478	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
4	1, 2, 3	syl2anc 661	1 |- ( ph -> ( A + B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 1758  (class class class)co 6203   CCcc 9394   + caddc 9399

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

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  cnegex  9664  addcom  9669  addcomd  9685  negeu  9714  addsubass  9734  subsub2  9751  subsub4  9756  pnpcan  9762  pnncan  9764  addsub4  9766  divdir  10131  cju  10432  cnref1o  11100  xov1plusxeqvd  11551  expaddz  12028  binom3  12105  spllen  12517  crre  12724  remullem  12738  imval2  12761  cjreim2  12771  sqreulem  12968  addcn2  13192  o1add  13212  fsumadd  13336  isumadd  13355  binomlem  13413  efaddlem  13499  ef4p  13518  cosf  13530  tanval2  13538  tanval3  13539  resin4p  13543  recos4p  13544  efival  13557  sinadd  13569  cosadd  13570  tanadd  13572  sadadd2lem2  13767  sadadd2lem  13776  pythagtriplem1  14004  pythagtriplem12  14014  pythagtriplem17  14019  pcbc  14083  mul4sqlem  14135  4sqlem14  14140  vdwlem6  14168  vdwlem9  14171  mulgdirlem  15773  blcvx  20510  tchcphlem1  20885  csbren  21033  ovollb2lem  21106  mbfadd  21275  itgcnlem  21403  itgaddlem2  21437  dvmptre  21579  dvsincos  21589  taylthlem2  21975  ptolemy  22094  tanregt0  22131  eff1olem  22140  cosargd  22193  tanarg  22204  logf1o2  22231  efopn  22239  cxpsqrlem  22283  cxpeq  22331  ang180lem1  22341  ang180lem2  22342  ang180lem3  22343  ang180lem4  22344  pythag  22349  ssscongptld  22356  chordthmlem  22363  chordthmlem2  22364  chordthmlem3  22365  chordthmlem4  22366  chordthmlem5  22367  heron  22369  quad2  22370  dcubic1lem  22374  dcubic2  22375  dcubic1  22376  dcubic  22377  mcubic  22378  cubic2  22379  cubic  22380  binom4  22381  dquartlem1  22382  dquartlem2  22383  dquart  22384  quart1cl  22385  quart1lem  22386  quart1  22387  quartlem1  22388  quartlem2  22389  quartlem3  22390  quartlem4  22391  quart  22392  asinlem3  22402  asinf  22403  asinneg  22417  efiasin  22419  asinsinlem  22422  asinsin  22423  asinbnd  22430  atanlogaddlem  22444  ftalem7  22552  basellem3  22556  bposlem9  22767  lgsquad2lem1  22833  dchrvmasumiflem2  22887  mulogsumlem  22916  mulog2sumlem1  22919  mulog2sumlem2  22920  mulog2sumlem3  22921  selberglem1  22930  selberg2  22936  selberg3lem1  22942  selbergr  22953  selberg3r  22954  pntrlog2bndlem1  22962  pntrlog2bndlem2  22963  pntrlog2bndlem5  22966  pntrlog2bndlem6  22968  pntrlog2bnd  22969  brbtwn2  23323  colinearalglem1  23324  colinearalglem2  23325  axeuclidlem  23380  axcontlem2  23383  axcontlem7  23388  axcontlem8  23389  4ipval2  24275  4ipval3  24279  dipcj  24284  golem1  25847  lt2addrd  26207  archirngz  26371  archiabllem2c  26377  cnre2csqima  26506  ballotlemsima  27062  dmgmaddnn0  27177  dmgmdivn0  27178  lgamgulmlem2  27180  lgamgulmlem3  27181  lgamgulmlem4  27182  lgamgulmlem5  27183  lgamgulmlem6  27184  lgamgulm2  27186  lgambdd  27187  lgamucov  27188  lgamcvg2  27205  gamcvg  27206  gamcvg2lem  27209  pnpncand  27558  iprodgam  27670  binomfallfaclem2  27707  bpoly4  28366  fsumcube  28367  itg2addnclem3  28613  itgaddnclem2  28619  itgaddnc  28620  ftc1anclem6  28640  ftc1anclem8  28642  dvasin  28648  areacirclem1  28652  areacirclem4  28655  areacirc  28657  pellexlem2  29339  pellexlem6  29343  pell1234qrreccl  29363  pell1234qrmulcl  29364  pell14qrdich  29378  rmxyneg  29429  rmxyadd  29430  jm2.19lem4  29509  jm2.26lem3  29518  itgpowd  29758  clim1fr1  29942  stoweidlem1  29964  stoweidlem11  29974  stoweidlem13  29976  wallispilem4  30031  wallispilem5  30032  wallispi  30033  wallispi2lem1  30034  wallispi2lem2  30035  wallispi2  30036  stirlinglem1  30037  stirlinglem3  30039  stirlinglem4  30040  stirlinglem5  30041  stirlinglem6  30042  stirlinglem7  30043  stirlinglem10  30046  stirlinglem11  30047  stirlinglem12  30048  stirlinglem13  30049  stirlinglem15  30051  sigaraf  30057  sigaras  30059  sinhpcosh  31423