Theorem addcld 8166

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 8124	. 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 2200  (class class class)co 6001   CCcc 7997   + caddc 8002

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

This theorem is referenced by:  muladd11r  8302  negeu  8337  addsubass  8356  subsub2  8374  subsub4  8379  pnpcan  8385  pnncan  8387  addsub4  8389  pnpncand  8521  apreim  8750  addext  8757  aprcl  8793  aptap  8797  divdirap  8844  recp1lt1  9046  cju  9108  cnref1o  9846  modsumfzodifsn  10618  expaddzap  10805  binom2  10873  binom3  10879  sqoddm1div8  10915  mulsubdivbinom2ap  10933  nn0opthlem1d  10942  reval  11360  imval  11361  crre  11368  remullem  11382  imval2  11405  cjreim2  11415  cnrecnv  11421  resqrexlemcalc1  11525  maxabslemab  11717  maxltsup  11729  max0addsup  11730  minabs  11747  bdtrilem  11750  bdtri  11751  addcn2  11821  fsumadd  11917  isumadd  11942  binomlem  11994  efaddlem  12185  ef4p  12205  cosval  12214  cosf  12216  tanval2ap  12224  tanval3ap  12225  resin4p  12229  recos4p  12230  efival  12243  sinadd  12247  cosadd  12248  tanaddap  12250  pythagtriplem1  12788  pythagtriplem12  12798  pythagtriplem16  12802  pythagtriplem17  12803  pcbc  12874  mul4sqlem  12916  4sqlem14  12927  oddennn  12963  mulgdirlem  13690  gsumfzconst  13878  gsumfzfsumlemm  14551  addccncf  15274  limcimolemlt  15338  dvaddxxbr  15375  plyaddlem1  15421  ptolemy  15498  rpcxpadd  15579  binom4  15653  lgsquad2lem1  15760  2lgslem3d1  15779  qdencn  16395  iooref1o  16402  apdifflemr  16415