Theorem addcld 10059

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

Syntax hints:   -> wi 4   e. wcel 1990  (class class class)co 6650   CCcc 9934   + caddc 9939

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

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  cnegex  10217  addcom  10222  addcomd  10238  muladd11r  10249  negeu  10271  addsubass  10291  subsub2  10309  subsub4  10314  pnpcan  10320  pnncan  10322  addsub4  10324  pnpncand  10452  divdir  10710  cju  11016  cnref1o  11827  xov1plusxeqvd  12318  expaddz  12904  binom3  12985  sqoddm1div8  13028  mulsubdivbinom2  13046  muldivbinom2  13047  spllen  13505  crre  13854  remullem  13868  imval2  13891  cjreim2  13901  sqreulem  14099  addcn2  14324  o1add  14344  fsumadd  14470  isumadd  14498  binomlem  14561  binomfallfaclem2  14771  bpoly4  14790  fsumcube  14791  efaddlem  14823  ef4p  14843  cosf  14855  tanval2  14863  tanval3  14864  resin4p  14868  recos4p  14869  efival  14882  sinadd  14894  cosadd  14895  tanadd  14897  pwp1fsum  15114  sadadd2lem2  15172  sadadd2lem  15181  pythagtriplem1  15521  pythagtriplem12  15531  pythagtriplem17  15536  pcbc  15604  mul4sqlem  15657  4sqlem14  15662  vdwlem6  15690  vdwlem9  15693  mulgdirlem  17572  blcvx  22601  tchcphlem1  23034  cphipval2  23040  4cphipval2  23041  csbren  23182  ovollb2lem  23256  mbfadd  23428  itgcnlem  23556  itgaddlem2  23590  dvmptre  23732  dvsincos  23744  taylthlem2  24128  ptolemy  24248  tanregt0  24285  eff1olem  24294  cosargd  24354  tanarg  24365  logf1o2  24396  efopn  24404  cxpsqrtlem  24448  cxpeq  24498  ang180lem1  24539  ang180lem2  24540  ang180lem3  24541  ang180lem4  24542  pythag  24547  ssscongptld  24552  chordthmlem  24559  chordthmlem2  24560  chordthmlem3  24561  chordthmlem4  24562  chordthmlem5  24563  heron  24565  quad2  24566  dcubic1lem  24570  dcubic2  24571  dcubic1  24572  dcubic  24573  mcubic  24574  cubic2  24575  cubic  24576  binom4  24577  dquartlem1  24578  dquartlem2  24579  dquart  24580  quart1cl  24581  quart1lem  24582  quart1  24583  quartlem1  24584  quartlem2  24585  quartlem3  24586  quartlem4  24587  quart  24588  asinlem3  24598  asinf  24599  asinneg  24613  efiasin  24615  asinsinlem  24618  asinsin  24619  asinbnd  24626  atanlogaddlem  24640  dmgmaddnn0  24753  dmgmdivn0  24754  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamgulm2  24762  lgambdd  24763  lgamucov  24764  lgamcvg2  24781  gamcvg  24782  gamcvg2lem  24785  ftalem7  24805  basellem3  24809  bposlem9  25017  lgsquad2lem1  25109  2lgslem3d1  25128  dchrvmasumiflem2  25191  mulogsumlem  25220  mulog2sumlem1  25223  mulog2sumlem2  25224  mulog2sumlem3  25225  selberglem1  25234  selberg2  25240  selberg3lem1  25246  selbergr  25257  selberg3r  25258  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  brbtwn2  25785  colinearalglem1  25786  colinearalglem2  25787  axeuclidlem  25842  axcontlem2  25845  axcontlem7  25850  axcontlem8  25851  finsumvtxdg2ssteplem4  26444  4ipval2  27563  dipcj  27569  golem1  29130  lt2addrd  29516  bhmafibid1  29644  bhmafibid2  29645  2sqmod  29648  archirngz  29743  archiabllem2c  29749  cnre2csqima  29957  ballotlemsima  30577  hgt750lemb  30734  iprodgam  31628  dnizphlfeqhlf  32466  dnibndlem9  32476  knoppndvlem16  32518  itg2addnclem3  33463  itgaddnclem2  33469  itgaddnc  33470  ftc1anclem6  33490  ftc1anclem8  33492  dvasin  33496  areacirclem1  33500  areacirclem4  33503  areacirc  33505  pellexlem2  37394  pellexlem6  37398  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell14qrdich  37433  rmxyneg  37485  rmxyadd  37486  jm2.19lem4  37559  jm2.26lem3  37568  itgpowd  37800  int-rightdistd  38483  binomcxplemnn0  38548  binomcxplemrat  38549  binomcxplemfrat  38550  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  sub2times  39485  clim1fr1  39833  limcperiod  39860  addlimc  39880  coseq0  40075  fprodaddrecnncnvlem  40123  dvxpaek  40155  dvnxpaek  40157  dvnmul  40158  itgiccshift  40196  itgperiod  40197  stoweidlem1  40218  stoweidlem11  40228  stoweidlem13  40230  wallispilem4  40285  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  wallispi2  40290  stirlinglem1  40291  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  stirlinglem15  40305  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkeritg  40319  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem18  40342  fourierdlem26  40350  fourierdlem30  40354  fourierdlem48  40371  fourierdlem49  40372  fourierdlem79  40402  fourierdlem83  40406  fourierdlem92  40415  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  smfmullem1  40998  sigaraf  41042  sigaras  41044  fmtnorec4  41461  fldivmod  42313  dignn0flhalflem1  42409  sinhpcosh  42481