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  8483  negeu  8518  addsubass  8537  subsub2  8555  subsub4  8560  pnpcan  8566  pnncan  8568  addsub4  8570  pnpncand  8702  apreim  8933  addext  8940  aprcl  8976  aptap  8980  divdirap  9029  recp1lt1  9231  cju  9293  cnref1o  10061  modsumfzodifsn  10846  expaddzap  11033  binom2  11101  binom3  11107  sqoddm1div8  11144  mulsubdivbinom2ap  11163  nn0opthlem1d  11172  reval  11628  imval  11629  crre  11636  remullem  11650  imval2  11673  cjreim2  11684  cnrecnv  11690  resqrexlemcalc1  11794  maxabslemab  11987  maxltsup  11999  max0addsup  12000  minabs  12017  bdtrilem  12021  bdtri  12022  addcn2  12092  fsumadd  12189  isumadd  12214  binomlem  12266  efaddlem  12457  ef4p  12477  cosval  12486  cosf  12488  tanval2ap  12496  tanval3ap  12497  resin4p  12501  recos4p  12502  efival  12515  sinadd  12519  cosadd  12520  tanaddap  12522  pythagtriplem1  13064  pythagtriplem12  13074  pythagtriplem16  13078  pythagtriplem17  13079  pcbc  13150  mul4sqlem  13192  4sqlem14  13203  ballotfilemsima  13308  oddennn  13332  mulgdirlem  14005  gzsumconst  14192  gsumfsum  14972  addccncf  15750  limcimolemlt  15814  dvaddxxbr  15851  plyaddlem1  15897  ptolemy  15975  rpcxpadd  16060  binom4  16138  pellexlem2  16149  lgsquad2lem1  16298  2lgslem3d1  16317  dichmul0orlem7  16857  qdencn  17170  iooref1o  17181  apdifflemr  17194  qdiff  17196