Theorem addcld 8177

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 8135	. 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 2200  (class class class)co 6007   CCcc 8008   + caddc 8013

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

This theorem is referenced by:  muladd11r  8313  negeu  8348  addsubass  8367  subsub2  8385  subsub4  8390  pnpcan  8396  pnncan  8398  addsub4  8400  pnpncand  8532  apreim  8761  addext  8768  aprcl  8804  aptap  8808  divdirap  8855  recp1lt1  9057  cju  9119  cnref1o  9858  modsumfzodifsn  10630  expaddzap  10817  binom2  10885  binom3  10891  sqoddm1div8  10927  mulsubdivbinom2ap  10945  nn0opthlem1d  10954  reval  11376  imval  11377  crre  11384  remullem  11398  imval2  11421  cjreim2  11431  cnrecnv  11437  resqrexlemcalc1  11541  maxabslemab  11733  maxltsup  11745  max0addsup  11746  minabs  11763  bdtrilem  11766  bdtri  11767  addcn2  11837  fsumadd  11933  isumadd  11958  binomlem  12010  efaddlem  12201  ef4p  12221  cosval  12230  cosf  12232  tanval2ap  12240  tanval3ap  12241  resin4p  12245  recos4p  12246  efival  12259  sinadd  12263  cosadd  12264  tanaddap  12266  pythagtriplem1  12804  pythagtriplem12  12814  pythagtriplem16  12818  pythagtriplem17  12819  pcbc  12890  mul4sqlem  12932  4sqlem14  12943  oddennn  12979  mulgdirlem  13706  gsumfzconst  13894  gsumfzfsumlemm  14567  addccncf  15290  limcimolemlt  15354  dvaddxxbr  15391  plyaddlem1  15437  ptolemy  15514  rpcxpadd  15595  binom4  15669  lgsquad2lem1  15776  2lgslem3d1  15795  qdencn  16483  iooref1o  16490  apdifflemr  16503