Theorem addcld 8345

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209  (class class class)co 6085   CCcc 8177   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addcl 8275

This theorem is used by:  muladd11r  8482  negeu  8517  addsubass  8536  subsub2  8554  subsub4  8559  pnpcan  8565  pnncan  8567  addsub4  8569  pnpncand  8701  apreim  8931  addext  8938  aprcl  8974  aptap  8978  divdirap  9027  recp1lt1  9229  cju  9291  cnref1o  10051  modsumfzodifsn  10833  expaddzap  11020  binom2  11088  binom3  11094  sqoddm1div8  11131  mulsubdivbinom2ap  11149  nn0opthlem1d  11158  reval  11614  imval  11615  crre  11622  remullem  11636  imval2  11659  cjreim2  11670  cnrecnv  11676  resqrexlemcalc1  11780  maxabslemab  11972  maxltsup  11984  max0addsup  11985  minabs  12002  bdtrilem  12005  bdtri  12006  addcn2  12076  fsumadd  12173  isumadd  12198  binomlem  12250  efaddlem  12441  ef4p  12461  cosval  12470  cosf  12472  tanval2ap  12480  tanval3ap  12481  resin4p  12485  recos4p  12486  efival  12499  sinadd  12503  cosadd  12504  tanaddap  12506  pythagtriplem1  13044  pythagtriplem12  13054  pythagtriplem16  13058  pythagtriplem17  13059  pcbc  13130  mul4sqlem  13172  4sqlem14  13183  ballotfilemsima  13259  oddennn  13283  mulgdirlem  13956  gzsumconst  14143  gsumfsum  14923  addccncf  15701  limcimolemlt  15765  dvaddxxbr  15802  plyaddlem1  15848  ptolemy  15925  rpcxpadd  16007  binom4  16081  pellexlem2  16092  lgsquad2lem1  16200  2lgslem3d1  16219  dichmul0orlem7  16759  qdencn  17072  iooref1o  17083  apdifflemr  17096  qdiff  17098