Theorem addcld 7778

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

Syntax hints:   -> wi 4   e. wcel 1480  (class class class)co 5767   CCcc 7611   + caddc 7616

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

This theorem is referenced by:  muladd11r  7911  negeu  7946  addsubass  7965  subsub2  7983  subsub4  7988  pnpcan  7994  pnncan  7996  addsub4  7998  pnpncand  8130  apreim  8358  addext  8365  aprcl  8401  divdirap  8450  recp1lt1  8650  cju  8712  cnref1o  9433  modsumfzodifsn  10162  expaddzap  10330  binom2  10396  binom3  10402  sqoddm1div8  10437  nn0opthlem1d  10459  reval  10614  imval  10615  crre  10622  remullem  10636  imval2  10659  cjreim2  10669  cnrecnv  10675  resqrexlemcalc1  10779  maxabslemab  10971  maxltsup  10983  max0addsup  10984  minabs  11000  bdtrilem  11003  bdtri  11004  addcn2  11072  fsumadd  11168  isumadd  11193  binomlem  11245  efaddlem  11369  ef4p  11389  cosval  11399  cosf  11401  tanval2ap  11409  tanval3ap  11410  resin4p  11414  recos4p  11415  efival  11428  sinadd  11432  cosadd  11433  tanaddap  11435  oddennn  11894  addccncf  12744  limcimolemlt  12791  dvaddxxbr  12823  ptolemy  12894  qdencn  13211