Theorem addcld 7980

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 7939	. 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 2148  (class class class)co 5878   CCcc 7812   + caddc 7817

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

This theorem is referenced by:  muladd11r  8116  negeu  8151  addsubass  8170  subsub2  8188  subsub4  8193  pnpcan  8199  pnncan  8201  addsub4  8203  pnpncand  8335  apreim  8563  addext  8570  aprcl  8606  aptap  8610  divdirap  8657  recp1lt1  8859  cju  8921  cnref1o  9653  modsumfzodifsn  10399  expaddzap  10567  binom2  10635  binom3  10641  sqoddm1div8  10677  mulsubdivbinom2ap  10694  nn0opthlem1d  10703  reval  10861  imval  10862  crre  10869  remullem  10883  imval2  10906  cjreim2  10916  cnrecnv  10922  resqrexlemcalc1  11026  maxabslemab  11218  maxltsup  11230  max0addsup  11231  minabs  11247  bdtrilem  11250  bdtri  11251  addcn2  11321  fsumadd  11417  isumadd  11442  binomlem  11494  efaddlem  11685  ef4p  11705  cosval  11714  cosf  11716  tanval2ap  11724  tanval3ap  11725  resin4p  11729  recos4p  11730  efival  11743  sinadd  11747  cosadd  11748  tanaddap  11750  pythagtriplem1  12268  pythagtriplem12  12278  pythagtriplem16  12282  pythagtriplem17  12283  pcbc  12352  mul4sqlem  12394  oddennn  12396  mulgdirlem  13020  addccncf  14226  limcimolemlt  14273  dvaddxxbr  14305  ptolemy  14385  rpcxpadd  14466  binom4  14537  qdencn  14916  iooref1o  14923  apdifflemr  14936