Theorem addcld 8258

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 8217	. 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 6028   CCcc 8090   + caddc 8095

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

This theorem is referenced by:  muladd11r  8394  negeu  8429  addsubass  8448  subsub2  8466  subsub4  8471  pnpcan  8477  pnncan  8479  addsub4  8481  pnpncand  8613  apreim  8842  addext  8849  aprcl  8885  aptap  8889  divdirap  8936  recp1lt1  9138  cju  9200  cnref1o  9946  modsumfzodifsn  10721  expaddzap  10908  binom2  10976  binom3  10982  sqoddm1div8  11018  mulsubdivbinom2ap  11036  nn0opthlem1d  11045  reval  11489  imval  11490  crre  11497  remullem  11511  imval2  11534  cjreim2  11544  cnrecnv  11550  resqrexlemcalc1  11654  maxabslemab  11846  maxltsup  11858  max0addsup  11859  minabs  11876  bdtrilem  11879  bdtri  11880  addcn2  11950  fsumadd  12047  isumadd  12072  binomlem  12124  efaddlem  12315  ef4p  12335  cosval  12344  cosf  12346  tanval2ap  12354  tanval3ap  12355  resin4p  12359  recos4p  12360  efival  12373  sinadd  12377  cosadd  12378  tanaddap  12380  pythagtriplem1  12918  pythagtriplem12  12928  pythagtriplem16  12932  pythagtriplem17  12933  pcbc  13004  mul4sqlem  13046  4sqlem14  13057  oddennn  13093  mulgdirlem  13820  gsumfzconst  14008  gsumfzfsumlemm  14683  addccncf  15411  limcimolemlt  15475  dvaddxxbr  15512  plyaddlem1  15558  ptolemy  15635  rpcxpadd  15716  binom4  15790  pellexlem2  15792  lgsquad2lem1  15900  2lgslem3d1  15919  qdencn  16755  iooref1o  16766  apdifflemr  16779  qdiff  16781