Theorem addcld 8199

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 8157	. 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 2202  (class class class)co 6018   CCcc 8030   + caddc 8035

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

This theorem is referenced by:  muladd11r  8335  negeu  8370  addsubass  8389  subsub2  8407  subsub4  8412  pnpcan  8418  pnncan  8420  addsub4  8422  pnpncand  8554  apreim  8783  addext  8790  aprcl  8826  aptap  8830  divdirap  8877  recp1lt1  9079  cju  9141  cnref1o  9885  modsumfzodifsn  10659  expaddzap  10846  binom2  10914  binom3  10920  sqoddm1div8  10956  mulsubdivbinom2ap  10974  nn0opthlem1d  10983  reval  11411  imval  11412  crre  11419  remullem  11433  imval2  11456  cjreim2  11466  cnrecnv  11472  resqrexlemcalc1  11576  maxabslemab  11768  maxltsup  11780  max0addsup  11781  minabs  11798  bdtrilem  11801  bdtri  11802  addcn2  11872  fsumadd  11969  isumadd  11994  binomlem  12046  efaddlem  12237  ef4p  12257  cosval  12266  cosf  12268  tanval2ap  12276  tanval3ap  12277  resin4p  12281  recos4p  12282  efival  12295  sinadd  12299  cosadd  12300  tanaddap  12302  pythagtriplem1  12840  pythagtriplem12  12850  pythagtriplem16  12854  pythagtriplem17  12855  pcbc  12926  mul4sqlem  12968  4sqlem14  12979  oddennn  13015  mulgdirlem  13742  gsumfzconst  13930  gsumfzfsumlemm  14604  addccncf  15327  limcimolemlt  15391  dvaddxxbr  15428  plyaddlem1  15474  ptolemy  15551  rpcxpadd  15632  binom4  15706  lgsquad2lem1  15813  2lgslem3d1  15832  qdencn  16648  iooref1o  16655  apdifflemr  16668