Theorem addcld 8351

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 8310	. 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 6088   CCcc 8183   + caddc 8188

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

This theorem is used by:  muladd11r  8489  negeu  8524  addsubass  8543  subsub2  8561  subsub4  8566  pnpcan  8572  pnncan  8574  addsub4  8576  pnpncand  8708  apreim  8939  addext  8946  aprcl  8982  aptap  8986  divdirap  9035  recp1lt1  9237  cju  9299  cnref1o  10068  modsumfzodifsn  10854  expaddzap  11041  binom2  11109  binom3  11115  sqoddm1div8  11152  mulsubdivbinom2ap  11171  nn0opthlem1d  11180  reval  11636  imval  11637  crre  11644  remullem  11658  imval2  11681  cjreim2  11692  cnrecnv  11698  resqrexlemcalc1  11802  maxabslemab  11995  maxltsup  12007  max0addsup  12008  minabs  12026  bdtrilem  12030  bdtri  12031  addcn2  12101  fsumadd  12198  isumadd  12223  binomlem  12275  efaddlem  12466  ef4p  12486  cosval  12495  cosf  12497  tanval2ap  12505  tanval3ap  12506  resin4p  12510  recos4p  12511  efival  12524  sinadd  12528  cosadd  12529  tanaddap  12531  pythagtriplem1  13073  pythagtriplem12  13083  pythagtriplem16  13087  pythagtriplem17  13088  pcbc  13159  mul4sqlem  13201  4sqlem14  13212  ballotfilemsima  13317  oddennn  13341  mulgdirlem  14015  gzsumconst  14233  gsumfsum  15032  addccncf  15826  limcimolemlt  15890  dvaddxxbr  15927  plyaddlem1  15973  ptolemy  16051  rpcxpadd  16138  binom4  16219  pellexlem2  16230  bposlem9  16319  lgsquad2lem1  16405  2lgslem3d1  16424  dichmul0orlem7  16964  qdencn  17278  iooref1o  17289  apdifflemr  17303  qdiff  17305