Theorem addcld 7568

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

Syntax hints:   -> wi 4   e. wcel 1439  (class class class)co 5666   CCcc 7409   + caddc 7414

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

This theorem is referenced by:  muladd11r  7699  negeu  7734  addsubass  7753  subsub2  7771  subsub4  7776  pnpcan  7782  pnncan  7784  addsub4  7786  pnpncand  7914  apreim  8141  addext  8148  divdirap  8225  recp1lt1  8421  cju  8482  cnref1o  9194  modsumfzodifsn  9864  ser3add  9996  expaddzap  10060  binom2  10126  binom3  10132  sqoddm1div8  10167  nn0opthlem1d  10189  reval  10344  imval  10345  crre  10352  remullem  10366  imval2  10389  cjreim2  10399  cnrecnv  10405  resqrexlemcalc1  10508  maxabslemab  10700  maxltsup  10712  max0addsup  10713  addcn2  10760  fsumadd  10861  isumadd  10886  binomlem  10938  efaddlem  11025  ef4p  11045  cosval  11055  cosf  11057  tanval2ap  11065  tanval3ap  11066  resin4p  11070  recos4p  11071  efival  11084  sinadd  11088  cosadd  11089  tanaddap  11091  oddennn  11544  qdencn  12187