Theorem addcld 9644

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

Syntax hints:   -> wi 4   e. wcel 1842  (class class class)co 6277   CCcc 9519   + caddc 9524

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

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

This theorem is referenced by:  cnegex  9794  addcom  9799  addcomd  9815  negeu  9845  addsubass  9865  subsub2  9882  subsub4  9887  pnpcan  9893  pnncan  9895  addsub4  9897  pnpncand  10021  divdir  10270  cju  10571  cnref1o  11259  xov1plusxeqvd  11718  expaddz  12252  binom3  12329  spllen  12784  crre  13094  remullem  13108  imval2  13131  cjreim2  13141  sqreulem  13339  addcn2  13563  o1add  13583  fsumadd  13708  isumadd  13731  binomlem  13790  binomfallfaclem2  13983  bpoly4  14002  fsumcube  14003  efaddlem  14035  ef4p  14055  cosf  14067  tanval2  14075  tanval3  14076  resin4p  14080  recos4p  14081  efival  14094  sinadd  14106  cosadd  14107  tanadd  14109  sadadd2lem2  14307  sadadd2lem  14316  pythagtriplem1  14547  pythagtriplem12  14557  pythagtriplem17  14562  pcbc  14626  mul4sqlem  14678  4sqlem14  14683  vdwlem6  14711  vdwlem9  14714  mulgdirlem  16488  blcvx  21593  tchcphlem1  21968  csbren  22116  ovollb2lem  22189  mbfadd  22358  itgcnlem  22486  itgaddlem2  22520  dvmptre  22662  dvsincos  22672  taylthlem2  23059  ptolemy  23179  tanregt0  23216  eff1olem  23225  cosargd  23285  tanarg  23296  logf1o2  23323  efopn  23331  cxpsqrtlem  23375  cxpeq  23425  ang180lem1  23466  ang180lem2  23467  ang180lem3  23468  ang180lem4  23469  pythag  23474  ssscongptld  23479  chordthmlem  23486  chordthmlem2  23487  chordthmlem3  23488  chordthmlem4  23489  chordthmlem5  23490  heron  23492  quad2  23493  dcubic1lem  23497  dcubic2  23498  dcubic1  23499  dcubic  23500  mcubic  23501  cubic2  23502  cubic  23503  binom4  23504  dquartlem1  23505  dquartlem2  23506  dquart  23507  quart1cl  23508  quart1lem  23509  quart1  23510  quartlem1  23511  quartlem2  23512  quartlem3  23513  quartlem4  23514  quart  23515  asinlem3  23525  asinf  23526  asinneg  23540  efiasin  23542  asinsinlem  23545  asinsin  23546  asinbnd  23553  atanlogaddlem  23567  dmgmaddnn0  23680  dmgmdivn0  23681  lgamgulmlem2  23683  lgamgulmlem3  23684  lgamgulmlem4  23685  lgamgulmlem5  23686  lgamgulmlem6  23687  lgamgulm2  23689  lgambdd  23690  lgamucov  23691  lgamcvg2  23708  gamcvg  23709  gamcvg2lem  23712  ftalem7  23731  basellem3  23735  bposlem9  23946  lgsquad2lem1  24012  dchrvmasumiflem2  24066  mulogsumlem  24095  mulog2sumlem1  24098  mulog2sumlem2  24099  mulog2sumlem3  24100  selberglem1  24109  selberg2  24115  selberg3lem1  24121  selbergr  24132  selberg3r  24133  pntrlog2bndlem1  24141  pntrlog2bndlem2  24142  pntrlog2bndlem5  24145  pntrlog2bndlem6  24147  pntrlog2bnd  24148  brbtwn2  24612  colinearalglem1  24613  colinearalglem2  24614  axeuclidlem  24669  axcontlem2  24672  axcontlem7  24677  axcontlem8  24678  4ipval2  26018  4ipval3  26022  dipcj  26027  golem1  27589  lt2addrd  27996  bhmafibid1  28070  bhmafibid2  28071  2sqmod  28074  archirngz  28171  archiabllem2c  28177  cnre2csqima  28332  ballotlemsima  28946  iprodgam  29938  itg2addnclem3  31421  itgaddnclem2  31427  itgaddnc  31428  ftc1anclem6  31448  ftc1anclem8  31450  dvasin  31454  areacirclem1  31458  areacirclem4  31461  areacirc  31463  pellexlem2  35107  pellexlem6  35111  pell1234qrreccl  35131  pell1234qrmulcl  35132  pell14qrdich  35146  rmxyneg  35197  rmxyadd  35198  jm2.19lem4  35276  jm2.26lem3  35285  itgpowd  35526  int-rightdistd  35992  binomcxplemnn0  36082  binomcxplemrat  36083  binomcxplemfrat  36084  binomcxplemdvbinom  36086  binomcxplemnotnn0  36089  sub2times  36809  clim1fr1  36956  limcperiod  36983  addlimc  37003  coseq0  37013  dvxpaek  37086  dvnxpaek  37088  dvnmul  37089  itgiccshift  37128  itgperiod  37129  stoweidlem1  37132  stoweidlem11  37142  stoweidlem13  37144  wallispilem4  37199  wallispilem5  37200  wallispi  37201  wallispi2lem1  37202  wallispi2lem2  37203  wallispi2  37204  stirlinglem1  37205  stirlinglem3  37207  stirlinglem4  37208  stirlinglem5  37209  stirlinglem6  37210  stirlinglem7  37211  stirlinglem10  37214  stirlinglem11  37215  stirlinglem12  37216  stirlinglem13  37217  stirlinglem15  37219  dirkerper  37227  dirkertrigeqlem1  37229  dirkertrigeqlem2  37230  dirkertrigeqlem3  37231  dirkeritg  37233  dirkercncflem2  37235  dirkercncflem4  37237  fourierdlem18  37256  fourierdlem26  37264  fourierdlem30  37268  fourierdlem48  37286  fourierdlem49  37287  fourierdlem79  37317  fourierdlem83  37321  fourierdlem92  37330  fourierdlem93  37331  fourierdlem103  37341  fourierdlem104  37342  fourierdlem111  37349  fourierdlem112  37350  sigaraf  37419  sigaras  37421  fldivmod  38622  dignn0flhalflem1  38727  sinhpcosh  38761