Theorem addcld 8127

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 8085	. 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 2178  (class class class)co 5967   CCcc 7958   + caddc 7963

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

This theorem is referenced by:  muladd11r  8263  negeu  8298  addsubass  8317  subsub2  8335  subsub4  8340  pnpcan  8346  pnncan  8348  addsub4  8350  pnpncand  8482  apreim  8711  addext  8718  aprcl  8754  aptap  8758  divdirap  8805  recp1lt1  9007  cju  9069  cnref1o  9807  modsumfzodifsn  10578  expaddzap  10765  binom2  10833  binom3  10839  sqoddm1div8  10875  mulsubdivbinom2ap  10893  nn0opthlem1d  10902  reval  11275  imval  11276  crre  11283  remullem  11297  imval2  11320  cjreim2  11330  cnrecnv  11336  resqrexlemcalc1  11440  maxabslemab  11632  maxltsup  11644  max0addsup  11645  minabs  11662  bdtrilem  11665  bdtri  11666  addcn2  11736  fsumadd  11832  isumadd  11857  binomlem  11909  efaddlem  12100  ef4p  12120  cosval  12129  cosf  12131  tanval2ap  12139  tanval3ap  12140  resin4p  12144  recos4p  12145  efival  12158  sinadd  12162  cosadd  12163  tanaddap  12165  pythagtriplem1  12703  pythagtriplem12  12713  pythagtriplem16  12717  pythagtriplem17  12718  pcbc  12789  mul4sqlem  12831  4sqlem14  12842  oddennn  12878  mulgdirlem  13604  gsumfzconst  13792  gsumfzfsumlemm  14464  addccncf  15187  limcimolemlt  15251  dvaddxxbr  15288  plyaddlem1  15334  ptolemy  15411  rpcxpadd  15492  binom4  15566  lgsquad2lem1  15673  2lgslem3d1  15692  qdencn  16168  iooref1o  16175  apdifflemr  16188