Theorem addcld 8094

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 8052	. 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 2176  (class class class)co 5946   CCcc 7925   + caddc 7930

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

This theorem is referenced by:  muladd11r  8230  negeu  8265  addsubass  8284  subsub2  8302  subsub4  8307  pnpcan  8313  pnncan  8315  addsub4  8317  pnpncand  8449  apreim  8678  addext  8685  aprcl  8721  aptap  8725  divdirap  8772  recp1lt1  8974  cju  9036  cnref1o  9774  modsumfzodifsn  10543  expaddzap  10730  binom2  10798  binom3  10804  sqoddm1div8  10840  mulsubdivbinom2ap  10858  nn0opthlem1d  10867  reval  11193  imval  11194  crre  11201  remullem  11215  imval2  11238  cjreim2  11248  cnrecnv  11254  resqrexlemcalc1  11358  maxabslemab  11550  maxltsup  11562  max0addsup  11563  minabs  11580  bdtrilem  11583  bdtri  11584  addcn2  11654  fsumadd  11750  isumadd  11775  binomlem  11827  efaddlem  12018  ef4p  12038  cosval  12047  cosf  12049  tanval2ap  12057  tanval3ap  12058  resin4p  12062  recos4p  12063  efival  12076  sinadd  12080  cosadd  12081  tanaddap  12083  pythagtriplem1  12621  pythagtriplem12  12631  pythagtriplem16  12635  pythagtriplem17  12636  pcbc  12707  mul4sqlem  12749  4sqlem14  12760  oddennn  12796  mulgdirlem  13522  gsumfzconst  13710  gsumfzfsumlemm  14382  addccncf  15105  limcimolemlt  15169  dvaddxxbr  15206  plyaddlem1  15252  ptolemy  15329  rpcxpadd  15410  binom4  15484  lgsquad2lem1  15591  2lgslem3d1  15610  qdencn  16003  iooref1o  16010  apdifflemr  16023