Theorem addcld 9397

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 9356	. 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 1756  (class class class)co 6086   CCcc 9272   + caddc 9277

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

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

This theorem is referenced by:  cnegex  9542  addcom  9547  addcomd  9563  negeu  9592  addsubass  9612  subsub2  9629  subsub4  9634  pnpcan  9640  pnncan  9642  addsub4  9644  divdir  10009  cju  10310  cnref1o  10978  xov1plusxeqvd  11423  expaddz  11900  binom3  11977  spllen  12388  crre  12595  remullem  12609  imval2  12632  cjreim2  12642  sqreulem  12839  addcn2  13063  o1add  13083  fsumadd  13207  isumadd  13226  binomlem  13284  efaddlem  13370  ef4p  13389  cosf  13401  tanval2  13409  tanval3  13410  resin4p  13414  recos4p  13415  efival  13428  sinadd  13440  cosadd  13441  tanadd  13443  sadadd2lem2  13638  sadadd2lem  13647  pythagtriplem1  13875  pythagtriplem12  13885  pythagtriplem17  13890  pcbc  13954  mul4sqlem  14006  4sqlem14  14011  vdwlem6  14039  vdwlem9  14042  mulgdirlem  15642  blcvx  20350  tchcphlem1  20725  csbren  20873  ovollb2lem  20946  mbfadd  21114  itgcnlem  21242  itgaddlem2  21276  dvmptre  21418  dvsincos  21428  taylthlem2  21814  ptolemy  21933  tanregt0  21970  eff1olem  21979  cosargd  22032  tanarg  22043  logf1o2  22070  efopn  22078  cxpsqrlem  22122  cxpeq  22170  ang180lem1  22180  ang180lem2  22181  ang180lem3  22182  ang180lem4  22183  pythag  22188  ssscongptld  22195  chordthmlem  22202  chordthmlem2  22203  chordthmlem3  22204  chordthmlem4  22205  chordthmlem5  22206  heron  22208  quad2  22209  dcubic1lem  22213  dcubic2  22214  dcubic1  22215  dcubic  22216  mcubic  22217  cubic2  22218  cubic  22219  binom4  22220  dquartlem1  22221  dquartlem2  22222  dquart  22223  quart1cl  22224  quart1lem  22225  quart1  22226  quartlem1  22227  quartlem2  22228  quartlem3  22229  quartlem4  22230  quart  22231  asinlem3  22241  asinf  22242  asinneg  22256  efiasin  22258  asinsinlem  22261  asinsin  22262  asinbnd  22269  atanlogaddlem  22283  ftalem7  22391  basellem3  22395  bposlem9  22606  lgsquad2lem1  22672  dchrvmasumiflem2  22726  mulogsumlem  22755  mulog2sumlem1  22758  mulog2sumlem2  22759  mulog2sumlem3  22760  selberglem1  22769  selberg2  22775  selberg3lem1  22781  selbergr  22792  selberg3r  22793  pntrlog2bndlem1  22801  pntrlog2bndlem2  22802  pntrlog2bndlem5  22805  pntrlog2bndlem6  22807  pntrlog2bnd  22808  brbtwn2  23102  colinearalglem1  23103  colinearalglem2  23104  axeuclidlem  23159  axcontlem2  23162  axcontlem7  23167  axcontlem8  23168  4ipval2  24054  4ipval3  24058  dipcj  24063  golem1  25626  lt2addrd  25987  archirngz  26157  archiabllem2c  26163  cnre2csqima  26293  ballotlemsima  26850  dmgmaddnn0  26965  dmgmdivn0  26966  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem4  26970  lgamgulmlem5  26971  lgamgulmlem6  26972  lgamgulm2  26974  lgambdd  26975  lgamucov  26976  lgamcvg2  26993  gamcvg  26994  gamcvg2lem  26997  pnpncand  27345  iprodgam  27457  binomfallfaclem2  27494  bpoly4  28153  fsumcube  28154  itg2addnclem3  28398  itgaddnclem2  28404  itgaddnc  28405  ftc1anclem6  28425  ftc1anclem8  28427  dvasin  28433  areacirclem1  28437  areacirclem4  28440  areacirc  28442  pellexlem2  29124  pellexlem6  29128  pell1234qrreccl  29148  pell1234qrmulcl  29149  pell14qrdich  29163  rmxyneg  29214  rmxyadd  29215  jm2.19lem4  29294  jm2.26lem3  29303  itgpowd  29543  clim1fr1  29727  stoweidlem1  29749  stoweidlem11  29759  stoweidlem13  29761  wallispilem4  29816  wallispilem5  29817  wallispi  29818  wallispi2lem1  29819  wallispi2lem2  29820  wallispi2  29821  stirlinglem1  29822  stirlinglem3  29824  stirlinglem4  29825  stirlinglem5  29826  stirlinglem6  29827  stirlinglem7  29828  stirlinglem10  29831  stirlinglem11  29832  stirlinglem12  29833  stirlinglem13  29834  stirlinglem15  29836  sigaraf  29842  sigaras  29844  sinhpcosh  30964