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  10067  modsumfzodifsn  10853  expaddzap  11040  binom2  11108  binom3  11114  sqoddm1div8  11151  mulsubdivbinom2ap  11170  nn0opthlem1d  11179  reval  11635  imval  11636  crre  11643  remullem  11657  imval2  11680  cjreim2  11691  cnrecnv  11697  resqrexlemcalc1  11801  maxabslemab  11994  maxltsup  12006  max0addsup  12007  minabs  12025  bdtrilem  12029  bdtri  12030  addcn2  12100  fsumadd  12197  isumadd  12222  binomlem  12274  efaddlem  12465  ef4p  12485  cosval  12494  cosf  12496  tanval2ap  12504  tanval3ap  12505  resin4p  12509  recos4p  12510  efival  12523  sinadd  12527  cosadd  12528  tanaddap  12530  pythagtriplem1  13072  pythagtriplem12  13082  pythagtriplem16  13086  pythagtriplem17  13087  pcbc  13158  mul4sqlem  13200  4sqlem14  13211  ballotfilemsima  13316  oddennn  13340  mulgdirlem  14014  gzsumconst  14232  gsumfsum  15031  addccncf  15843  limcimolemlt  15907  dvaddxxbr  15944  plyaddlem1  15990  ptolemy  16068  rpcxpadd  16155  binom4  16236  pellexlem2  16247  bposlem9  16336  lgsquad2lem1  16422  2lgslem3d1  16441  dichmul0orlem7  16981  qdencn  17295  iooref1o  17306  apdifflemr  17320  qdiff  17322