Theorem addcld 8346

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209  (class class class)co 6085   CCcc 8178   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addcl 8276

This theorem is used by:  muladd11r  8484  negeu  8519  addsubass  8538  subsub2  8556  subsub4  8561  pnpcan  8567  pnncan  8569  addsub4  8571  pnpncand  8703  apreim  8934  addext  8941  aprcl  8977  aptap  8981  divdirap  9030  recp1lt1  9232  cju  9294  cnref1o  10062  modsumfzodifsn  10848  expaddzap  11035  binom2  11103  binom3  11109  sqoddm1div8  11146  mulsubdivbinom2ap  11165  nn0opthlem1d  11174  reval  11630  imval  11631  crre  11638  remullem  11652  imval2  11675  cjreim2  11686  cnrecnv  11692  resqrexlemcalc1  11796  maxabslemab  11989  maxltsup  12001  max0addsup  12002  minabs  12020  bdtrilem  12024  bdtri  12025  addcn2  12095  fsumadd  12192  isumadd  12217  binomlem  12269  efaddlem  12460  ef4p  12480  cosval  12489  cosf  12491  tanval2ap  12499  tanval3ap  12500  resin4p  12504  recos4p  12505  efival  12518  sinadd  12522  cosadd  12523  tanaddap  12525  pythagtriplem1  13067  pythagtriplem12  13077  pythagtriplem16  13081  pythagtriplem17  13082  pcbc  13153  mul4sqlem  13195  4sqlem14  13206  ballotfilemsima  13311  oddennn  13335  mulgdirlem  14009  gzsumconst  14227  gsumfsum  15007  addccncf  15792  limcimolemlt  15856  dvaddxxbr  15893  plyaddlem1  15939  ptolemy  16017  rpcxpadd  16102  binom4  16180  pellexlem2  16191  bposlem9  16280  lgsquad2lem1  16366  2lgslem3d1  16385  dichmul0orlem7  16925  qdencn  17238  iooref1o  17249  apdifflemr  17263  qdiff  17265