Theorem addcld 9393

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

Syntax hints:   -> wi 4   e. wcel 1755  (class class class)co 6080   CCcc 9268   + caddc 9273

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

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

This theorem is referenced by:  cnegex  9538  addcom  9543  addcomd  9559  negeu  9588  addsubass  9608  subsub2  9625  subsub4  9630  pnpcan  9636  pnncan  9638  addsub4  9640  divdir  10005  cju  10306  cnref1o  10974  xov1plusxeqvd  11418  expaddz  11892  binom3  11969  spllen  12380  crre  12587  remullem  12601  imval2  12624  cjreim2  12634  sqreulem  12831  addcn2  13055  o1add  13075  fsumadd  13199  isumadd  13218  binomlem  13275  efaddlem  13361  ef4p  13380  cosf  13392  tanval2  13400  tanval3  13401  resin4p  13405  recos4p  13406  efival  13419  sinadd  13431  cosadd  13432  tanadd  13434  sadadd2lem2  13629  sadadd2lem  13638  pythagtriplem1  13866  pythagtriplem12  13876  pythagtriplem17  13881  pcbc  13945  mul4sqlem  13997  4sqlem14  14002  vdwlem6  14030  vdwlem9  14033  mulgdirlem  15631  blcvx  20217  tchcphlem1  20592  csbren  20740  ovollb2lem  20813  mbfadd  20981  itgcnlem  21109  itgaddlem2  21143  dvmptre  21285  dvsincos  21295  taylthlem2  21724  ptolemy  21843  tanregt0  21880  eff1olem  21889  cosargd  21942  tanarg  21953  logf1o2  21980  efopn  21988  cxpsqrlem  22032  cxpeq  22080  ang180lem1  22090  ang180lem2  22091  ang180lem3  22092  ang180lem4  22093  pythag  22098  ssscongptld  22105  chordthmlem  22112  chordthmlem2  22113  chordthmlem3  22114  chordthmlem4  22115  chordthmlem5  22116  heron  22118  quad2  22119  dcubic1lem  22123  dcubic2  22124  dcubic1  22125  dcubic  22126  mcubic  22127  cubic2  22128  cubic  22129  binom4  22130  dquartlem1  22131  dquartlem2  22132  dquart  22133  quart1cl  22134  quart1lem  22135  quart1  22136  quartlem1  22137  quartlem2  22138  quartlem3  22139  quartlem4  22140  quart  22141  asinlem3  22151  asinf  22152  asinneg  22166  efiasin  22168  asinsinlem  22171  asinsin  22172  asinbnd  22179  atanlogaddlem  22193  ftalem7  22301  basellem3  22305  bposlem9  22516  lgsquad2lem1  22582  dchrvmasumiflem2  22636  mulogsumlem  22665  mulog2sumlem1  22668  mulog2sumlem2  22669  mulog2sumlem3  22670  selberglem1  22679  selberg2  22685  selberg3lem1  22691  selbergr  22702  selberg3r  22703  pntrlog2bndlem1  22711  pntrlog2bndlem2  22712  pntrlog2bndlem5  22715  pntrlog2bndlem6  22717  pntrlog2bnd  22718  brbtwn2  22974  colinearalglem1  22975  colinearalglem2  22976  axeuclidlem  23031  axcontlem2  23034  axcontlem7  23039  axcontlem8  23040  4ipval2  23926  4ipval3  23930  dipcj  23935  golem1  25498  lt2addrd  25861  archirngz  26030  archiabllem2c  26036  cnre2csqima  26195  ballotlemsima  26746  dmgmaddnn0  26861  dmgmdivn0  26862  lgamgulmlem2  26864  lgamgulmlem3  26865  lgamgulmlem4  26866  lgamgulmlem5  26867  lgamgulmlem6  26868  lgamgulm2  26870  lgambdd  26871  lgamucov  26872  lgamcvg2  26889  gamcvg  26890  gamcvg2lem  26893  pnpncand  27241  iprodgam  27353  binomfallfaclem2  27390  bpoly4  28049  fsumcube  28050  itg2addnclem3  28289  itgaddnclem2  28295  itgaddnc  28296  ftc1anclem6  28316  ftc1anclem8  28318  dvasin  28324  areacirclem1  28328  areacirclem4  28331  areacirc  28333  pellexlem2  29016  pellexlem6  29020  pell1234qrreccl  29040  pell1234qrmulcl  29041  pell14qrdich  29055  rmxyneg  29106  rmxyadd  29107  jm2.19lem4  29186  jm2.26lem3  29195  itgpowd  29435  clim1fr1  29620  stoweidlem1  29642  stoweidlem11  29652  stoweidlem13  29654  wallispilem4  29709  wallispilem5  29710  wallispi  29711  wallispi2lem1  29712  wallispi2lem2  29713  wallispi2  29714  stirlinglem1  29715  stirlinglem3  29717  stirlinglem4  29718  stirlinglem5  29719  stirlinglem6  29720  stirlinglem7  29721  stirlinglem10  29724  stirlinglem11  29725  stirlinglem12  29726  stirlinglem13  29727  stirlinglem15  29729  sigaraf  29735  sigaras  29737  sinhpcosh  30784