Theorem addcld 8309

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 8268	. 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 2205  (class class class)co 6058   CCcc 8141   + caddc 8146

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

This theorem is referenced by:  muladd11r  8445  negeu  8480  addsubass  8499  subsub2  8517  subsub4  8522  pnpcan  8528  pnncan  8530  addsub4  8532  pnpncand  8664  apreim  8894  addext  8901  aprcl  8937  aptap  8941  divdirap  8988  recp1lt1  9190  cju  9252  cnref1o  10001  modsumfzodifsn  10782  expaddzap  10969  binom2  11037  binom3  11043  sqoddm1div8  11080  mulsubdivbinom2ap  11098  nn0opthlem1d  11107  reval  11559  imval  11560  crre  11567  remullem  11581  imval2  11604  cjreim2  11614  cnrecnv  11620  resqrexlemcalc1  11724  maxabslemab  11916  maxltsup  11928  max0addsup  11929  minabs  11946  bdtrilem  11949  bdtri  11950  addcn2  12020  fsumadd  12117  isumadd  12142  binomlem  12194  efaddlem  12385  ef4p  12405  cosval  12414  cosf  12416  tanval2ap  12424  tanval3ap  12425  resin4p  12429  recos4p  12430  efival  12443  sinadd  12447  cosadd  12448  tanaddap  12450  pythagtriplem1  12988  pythagtriplem12  12998  pythagtriplem16  13002  pythagtriplem17  13003  pcbc  13074  mul4sqlem  13116  4sqlem14  13127  ballotfilemsima  13203  oddennn  13227  mulgdirlem  13906  gsumfzconst  14094  gsumfzfsumlemm  14861  addccncf  15591  limcimolemlt  15655  dvaddxxbr  15692  plyaddlem1  15738  ptolemy  15815  rpcxpadd  15896  binom4  15970  pellexlem2  15972  lgsquad2lem1  16080  2lgslem3d1  16099  qdencn  16933  iooref1o  16944  apdifflemr  16957  qdiff  16959