Theorem addcld 9618

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 9577	. 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 1804  (class class class)co 6281   CCcc 9493   + caddc 9498

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

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

This theorem is referenced by:  cnegex  9764  addcom  9769  addcomd  9785  negeu  9815  addsubass  9835  subsub2  9852  subsub4  9857  pnpcan  9863  pnncan  9865  addsub4  9867  pnpncand  9988  divdir  10237  cju  10539  cnref1o  11226  xov1plusxeqvd  11677  expaddz  12192  binom3  12269  spllen  12712  crre  12929  remullem  12943  imval2  12966  cjreim2  12976  sqreulem  13174  addcn2  13398  o1add  13418  fsumadd  13543  isumadd  13564  binomlem  13623  efaddlem  13810  ef4p  13830  cosf  13842  tanval2  13850  tanval3  13851  resin4p  13855  recos4p  13856  efival  13869  sinadd  13881  cosadd  13882  tanadd  13884  sadadd2lem2  14082  sadadd2lem  14091  pythagtriplem1  14322  pythagtriplem12  14332  pythagtriplem17  14337  pcbc  14401  mul4sqlem  14453  4sqlem14  14458  vdwlem6  14486  vdwlem9  14489  mulgdirlem  16145  blcvx  21281  tchcphlem1  21656  csbren  21804  ovollb2lem  21877  mbfadd  22046  itgcnlem  22174  itgaddlem2  22208  dvmptre  22350  dvsincos  22360  taylthlem2  22747  ptolemy  22867  tanregt0  22904  eff1olem  22913  cosargd  22971  tanarg  22982  logf1o2  23009  efopn  23017  cxpsqrtlem  23061  cxpeq  23109  ang180lem1  23119  ang180lem2  23120  ang180lem3  23121  ang180lem4  23122  pythag  23127  ssscongptld  23134  chordthmlem  23141  chordthmlem2  23142  chordthmlem3  23143  chordthmlem4  23144  chordthmlem5  23145  heron  23147  quad2  23148  dcubic1lem  23152  dcubic2  23153  dcubic1  23154  dcubic  23155  mcubic  23156  cubic2  23157  cubic  23158  binom4  23159  dquartlem1  23160  dquartlem2  23161  dquart  23162  quart1cl  23163  quart1lem  23164  quart1  23165  quartlem1  23166  quartlem2  23167  quartlem3  23168  quartlem4  23169  quart  23170  asinlem3  23180  asinf  23181  asinneg  23195  efiasin  23197  asinsinlem  23200  asinsin  23201  asinbnd  23208  atanlogaddlem  23222  ftalem7  23330  basellem3  23334  bposlem9  23545  lgsquad2lem1  23611  dchrvmasumiflem2  23665  mulogsumlem  23694  mulog2sumlem1  23697  mulog2sumlem2  23698  mulog2sumlem3  23699  selberglem1  23708  selberg2  23714  selberg3lem1  23720  selbergr  23731  selberg3r  23732  pntrlog2bndlem1  23740  pntrlog2bndlem2  23741  pntrlog2bndlem5  23744  pntrlog2bndlem6  23746  pntrlog2bnd  23747  brbtwn2  24186  colinearalglem1  24187  colinearalglem2  24188  axeuclidlem  24243  axcontlem2  24246  axcontlem7  24251  axcontlem8  24252  4ipval2  25596  4ipval3  25600  dipcj  25605  golem1  27168  lt2addrd  27541  bhmafibid1  27610  bhmafibid2  27611  2sqmod  27614  archirngz  27711  archiabllem2c  27717  cnre2csqima  27871  ballotlemsima  28432  dmgmaddnn0  28547  dmgmdivn0  28548  lgamgulmlem2  28550  lgamgulmlem3  28551  lgamgulmlem4  28552  lgamgulmlem5  28553  lgamgulmlem6  28554  lgamgulm2  28556  lgambdd  28557  lgamucov  28558  lgamcvg2  28575  gamcvg  28576  gamcvg2lem  28579  iprodgam  29101  binomfallfaclem2  29138  bpoly4  29797  fsumcube  29798  itg2addnclem3  30044  itgaddnclem2  30050  itgaddnc  30051  ftc1anclem6  30071  ftc1anclem8  30073  dvasin  30079  areacirclem1  30083  areacirclem4  30086  areacirc  30088  pellexlem2  30742  pellexlem6  30746  pell1234qrreccl  30766  pell1234qrmulcl  30767  pell14qrdich  30781  rmxyneg  30832  rmxyadd  30833  jm2.19lem4  30910  jm2.26lem3  30919  itgpowd  31158  sub2times  31409  clim1fr1  31561  limcperiod  31588  addlimc  31608  coseq0  31618  dvxpaek  31691  dvnxpaek  31693  dvnmul  31694  itgiccshift  31733  itgperiod  31734  stoweidlem1  31737  stoweidlem11  31747  stoweidlem13  31749  wallispilem4  31804  wallispilem5  31805  wallispi  31806  wallispi2lem1  31807  wallispi2lem2  31808  wallispi2  31809  stirlinglem1  31810  stirlinglem3  31812  stirlinglem4  31813  stirlinglem5  31814  stirlinglem6  31815  stirlinglem7  31816  stirlinglem10  31819  stirlinglem11  31820  stirlinglem12  31821  stirlinglem13  31822  stirlinglem15  31824  dirkerper  31832  dirkertrigeqlem1  31834  dirkertrigeqlem2  31835  dirkertrigeqlem3  31836  dirkeritg  31838  dirkercncflem2  31840  dirkercncflem4  31842  fourierdlem18  31861  fourierdlem26  31869  fourierdlem30  31873  fourierdlem48  31891  fourierdlem49  31892  fourierdlem79  31922  fourierdlem83  31926  fourierdlem92  31935  fourierdlem93  31936  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  fourierdlem112  31955  sigaraf  32024  sigaras  32026  sinhpcosh  33004