Theorem addcld 9614

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 9573	. 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 1767  (class class class)co 6283   CCcc 9489   + caddc 9494

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

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

This theorem is referenced by:  cnegex  9759  addcom  9764  addcomd  9780  negeu  9809  addsubass  9829  subsub2  9846  subsub4  9851  pnpcan  9857  pnncan  9859  addsub4  9861  divdir  10229  cju  10531  cnref1o  11214  xov1plusxeqvd  11665  expaddz  12177  binom3  12254  spllen  12692  crre  12909  remullem  12923  imval2  12946  cjreim2  12956  sqreulem  13154  addcn2  13378  o1add  13398  fsumadd  13523  isumadd  13544  binomlem  13603  efaddlem  13689  ef4p  13708  cosf  13720  tanval2  13728  tanval3  13729  resin4p  13733  recos4p  13734  efival  13747  sinadd  13759  cosadd  13760  tanadd  13762  sadadd2lem2  13958  sadadd2lem  13967  pythagtriplem1  14198  pythagtriplem12  14208  pythagtriplem17  14213  pcbc  14277  mul4sqlem  14329  4sqlem14  14334  vdwlem6  14362  vdwlem9  14365  mulgdirlem  15973  blcvx  21054  tchcphlem1  21429  csbren  21577  ovollb2lem  21650  mbfadd  21819  itgcnlem  21947  itgaddlem2  21981  dvmptre  22123  dvsincos  22133  taylthlem2  22519  ptolemy  22638  tanregt0  22675  eff1olem  22684  cosargd  22737  tanarg  22748  logf1o2  22775  efopn  22783  cxpsqrtlem  22827  cxpeq  22875  ang180lem1  22885  ang180lem2  22886  ang180lem3  22887  ang180lem4  22888  pythag  22893  ssscongptld  22900  chordthmlem  22907  chordthmlem2  22908  chordthmlem3  22909  chordthmlem4  22910  chordthmlem5  22911  heron  22913  quad2  22914  dcubic1lem  22918  dcubic2  22919  dcubic1  22920  dcubic  22921  mcubic  22922  cubic2  22923  cubic  22924  binom4  22925  dquartlem1  22926  dquartlem2  22927  dquart  22928  quart1cl  22929  quart1lem  22930  quart1  22931  quartlem1  22932  quartlem2  22933  quartlem3  22934  quartlem4  22935  quart  22936  asinlem3  22946  asinf  22947  asinneg  22961  efiasin  22963  asinsinlem  22966  asinsin  22967  asinbnd  22974  atanlogaddlem  22988  ftalem7  23096  basellem3  23100  bposlem9  23311  lgsquad2lem1  23377  dchrvmasumiflem2  23431  mulogsumlem  23460  mulog2sumlem1  23463  mulog2sumlem2  23464  mulog2sumlem3  23465  selberglem1  23474  selberg2  23480  selberg3lem1  23486  selbergr  23497  selberg3r  23498  pntrlog2bndlem1  23506  pntrlog2bndlem2  23507  pntrlog2bndlem5  23510  pntrlog2bndlem6  23512  pntrlog2bnd  23513  brbtwn2  23900  colinearalglem1  23901  colinearalglem2  23902  axeuclidlem  23957  axcontlem2  23960  axcontlem7  23965  axcontlem8  23966  4ipval2  25310  4ipval3  25314  dipcj  25319  golem1  26882  lt2addrd  27247  archirngz  27411  archiabllem2c  27417  cnre2csqima  27545  ballotlemsima  28110  dmgmaddnn0  28225  dmgmdivn0  28226  lgamgulmlem2  28228  lgamgulmlem3  28229  lgamgulmlem4  28230  lgamgulmlem5  28231  lgamgulmlem6  28232  lgamgulm2  28234  lgambdd  28235  lgamucov  28236  lgamcvg2  28253  gamcvg  28254  gamcvg2lem  28257  pnpncand  28606  iprodgam  28718  binomfallfaclem2  28755  bpoly4  29414  fsumcube  29415  itg2addnclem3  29661  itgaddnclem2  29667  itgaddnc  29668  ftc1anclem6  29688  ftc1anclem8  29690  dvasin  29696  areacirclem1  29700  areacirclem4  29703  areacirc  29705  pellexlem2  30386  pellexlem6  30390  pell1234qrreccl  30410  pell1234qrmulcl  30411  pell14qrdich  30425  rmxyneg  30476  rmxyadd  30477  jm2.19lem4  30554  jm2.26lem3  30563  itgpowd  30803  sub2times  31048  clim1fr1  31159  limcperiod  31186  addlimc  31206  coseq0  31215  itgiccshift  31314  itgperiod  31315  stoweidlem1  31317  stoweidlem11  31327  stoweidlem13  31329  wallispilem4  31384  wallispilem5  31385  wallispi  31386  wallispi2lem1  31387  wallispi2lem2  31388  wallispi2  31389  stirlinglem1  31390  stirlinglem3  31392  stirlinglem4  31393  stirlinglem5  31394  stirlinglem6  31395  stirlinglem7  31396  stirlinglem10  31399  stirlinglem11  31400  stirlinglem12  31401  stirlinglem13  31402  stirlinglem15  31404  dirkerper  31412  dirkertrigeqlem1  31414  dirkertrigeqlem2  31415  dirkertrigeqlem3  31416  dirkeritg  31418  dirkercncflem2  31420  dirkercncflem4  31422  fourierdlem18  31441  fourierdlem26  31449  fourierdlem30  31453  fourierdlem48  31471  fourierdlem49  31472  fourierdlem83  31506  fourierdlem92  31515  fourierdlem93  31516  fourierdlem103  31526  fourierdlem104  31527  fourierdlem111  31534  sigaraf  31553  sigaras  31555  sinhpcosh  32224