Theorem addcld 8199

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

Syntax hints:   -> wi 4   e. wcel 2202  (class class class)co 6018   CCcc 8030   + caddc 8035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addcl 8128

This theorem is referenced by:  muladd11r  8335  negeu  8370  addsubass  8389  subsub2  8407  subsub4  8412  pnpcan  8418  pnncan  8420  addsub4  8422  pnpncand  8554  apreim  8783  addext  8790  aprcl  8826  aptap  8830  divdirap  8877  recp1lt1  9079  cju  9141  cnref1o  9885  modsumfzodifsn  10659  expaddzap  10846  binom2  10914  binom3  10920  sqoddm1div8  10956  mulsubdivbinom2ap  10974  nn0opthlem1d  10983  reval  11427  imval  11428  crre  11435  remullem  11449  imval2  11472  cjreim2  11482  cnrecnv  11488  resqrexlemcalc1  11592  maxabslemab  11784  maxltsup  11796  max0addsup  11797  minabs  11814  bdtrilem  11817  bdtri  11818  addcn2  11888  fsumadd  11985  isumadd  12010  binomlem  12062  efaddlem  12253  ef4p  12273  cosval  12282  cosf  12284  tanval2ap  12292  tanval3ap  12293  resin4p  12297  recos4p  12298  efival  12311  sinadd  12315  cosadd  12316  tanaddap  12318  pythagtriplem1  12856  pythagtriplem12  12866  pythagtriplem16  12870  pythagtriplem17  12871  pcbc  12942  mul4sqlem  12984  4sqlem14  12995  oddennn  13031  mulgdirlem  13758  gsumfzconst  13946  gsumfzfsumlemm  14620  addccncf  15343  limcimolemlt  15407  dvaddxxbr  15444  plyaddlem1  15490  ptolemy  15567  rpcxpadd  15648  binom4  15722  lgsquad2lem1  15829  2lgslem3d1  15848  qdencn  16682  iooref1o  16689  apdifflemr  16702  qdiff  16704