Theorem addcld 9662

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 9621	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
4	1, 2, 3	syl2anc 667	1 |- ( ph -> ( A + B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 1887  (class class class)co 6290   CCcc 9537   + caddc 9542

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

This theorem depends on definitions:  df-bi 189  df-an 373

This theorem is referenced by:  cnegex  9814  addcom  9819  addcomd  9835  negeu  9865  addsubass  9885  subsub2  9902  subsub4  9907  pnpcan  9913  pnncan  9915  addsub4  9917  pnpncand  10041  divdir  10293  cju  10605  cnref1o  11297  xov1plusxeqvd  11778  expaddz  12316  binom3  12393  spllen  12861  crre  13177  remullem  13191  imval2  13214  cjreim2  13224  sqreulem  13422  addcn2  13657  o1add  13677  fsumadd  13805  isumadd  13828  binomlem  13887  binomfallfaclem2  14093  bpoly4  14112  fsumcube  14113  efaddlem  14147  ef4p  14167  cosf  14179  tanval2  14187  tanval3  14188  resin4p  14192  recos4p  14193  efival  14206  sinadd  14218  cosadd  14219  tanadd  14221  sadadd2lem2  14424  sadadd2lem  14433  pythagtriplem1  14766  pythagtriplem12  14776  pythagtriplem17  14781  pcbc  14845  mul4sqlem  14897  4sqlem14OLD  14902  4sqlem14  14908  vdwlem6  14936  vdwlem9  14939  mulgdirlem  16782  blcvx  21816  tchcphlem1  22209  csbren  22353  ovollb2lem  22441  mbfadd  22617  itgcnlem  22747  itgaddlem2  22781  dvmptre  22923  dvsincos  22933  taylthlem2  23329  ptolemy  23451  tanregt0  23488  eff1olem  23497  cosargd  23557  tanarg  23568  logf1o2  23595  efopn  23603  cxpsqrtlem  23647  cxpeq  23697  ang180lem1  23738  ang180lem2  23739  ang180lem3  23740  ang180lem4  23741  pythag  23746  ssscongptld  23751  chordthmlem  23758  chordthmlem2  23759  chordthmlem3  23760  chordthmlem4  23761  chordthmlem5  23762  heron  23764  quad2  23765  dcubic1lem  23769  dcubic2  23770  dcubic1  23771  dcubic  23772  mcubic  23773  cubic2  23774  cubic  23775  binom4  23776  dquartlem1  23777  dquartlem2  23778  dquart  23779  quart1cl  23780  quart1lem  23781  quart1  23782  quartlem1  23783  quartlem2  23784  quartlem3  23785  quartlem4  23786  quart  23787  asinlem3  23797  asinf  23798  asinneg  23812  efiasin  23814  asinsinlem  23817  asinsin  23818  asinbnd  23825  atanlogaddlem  23839  dmgmaddnn0  23952  dmgmdivn0  23953  lgamgulmlem2  23955  lgamgulmlem3  23956  lgamgulmlem4  23957  lgamgulmlem5  23958  lgamgulmlem6  23959  lgamgulm2  23961  lgambdd  23962  lgamucov  23963  lgamcvg2  23980  gamcvg  23981  gamcvg2lem  23984  ftalem7  24005  basellem3  24009  bposlem9  24220  lgsquad2lem1  24286  dchrvmasumiflem2  24340  mulogsumlem  24369  mulog2sumlem1  24372  mulog2sumlem2  24373  mulog2sumlem3  24374  selberglem1  24383  selberg2  24389  selberg3lem1  24395  selbergr  24406  selberg3r  24407  pntrlog2bndlem1  24415  pntrlog2bndlem2  24416  pntrlog2bndlem5  24419  pntrlog2bndlem6  24421  pntrlog2bnd  24422  brbtwn2  24935  colinearalglem1  24936  colinearalglem2  24937  axeuclidlem  24992  axcontlem2  24995  axcontlem7  25000  axcontlem8  25001  4ipval2  26344  4ipval3  26348  dipcj  26353  golem1  27924  lt2addrd  28326  bhmafibid1  28405  bhmafibid2  28406  2sqmod  28409  archirngz  28506  archiabllem2c  28512  cnre2csqima  28717  ballotlemsima  29348  ballotlemsimaOLD  29386  iprodgam  30378  itg2addnclem3  31995  itgaddnclem2  32001  itgaddnc  32002  ftc1anclem6  32022  ftc1anclem8  32024  dvasin  32028  areacirclem1  32032  areacirclem4  32035  areacirc  32037  pellexlem2  35674  pellexlem6  35678  pell1234qrreccl  35700  pell1234qrmulcl  35701  pell14qrdich  35715  rmxyneg  35768  rmxyadd  35769  jm2.19lem4  35847  jm2.26lem3  35856  itgpowd  36099  int-rightdistd  36627  binomcxplemnn0  36698  binomcxplemrat  36699  binomcxplemfrat  36700  binomcxplemdvbinom  36702  binomcxplemnotnn0  36705  sub2times  37483  clim1fr1  37679  limcperiod  37708  addlimc  37729  coseq0  37739  dvxpaek  37815  dvnxpaek  37817  dvnmul  37818  itgiccshift  37857  itgperiod  37858  stoweidlem1  37861  stoweidlem11  37871  stoweidlem13  37873  wallispilem4  37930  wallispilem5  37931  wallispi  37932  wallispi2lem1  37933  wallispi2lem2  37934  wallispi2  37935  stirlinglem1  37936  stirlinglem3  37938  stirlinglem4  37939  stirlinglem5  37940  stirlinglem6  37941  stirlinglem7  37942  stirlinglem10  37945  stirlinglem11  37946  stirlinglem12  37947  stirlinglem13  37948  stirlinglem15  37950  dirkerper  37958  dirkertrigeqlem1  37960  dirkertrigeqlem2  37961  dirkertrigeqlem3  37962  dirkeritg  37964  dirkercncflem2  37966  dirkercncflem4  37968  fourierdlem18  37987  fourierdlem26  37995  fourierdlem30  37999  fourierdlem48  38018  fourierdlem49  38019  fourierdlem79  38049  fourierdlem83  38053  fourierdlem92  38062  fourierdlem93  38063  fourierdlem103  38073  fourierdlem104  38074  fourierdlem111  38081  fourierdlem112  38082  sigaraf  38462  sigaras  38464  fldivmod  40374  dignn0flhalflem1  40479  sinhpcosh  40513