Theorem addcl 8304

Description: Alias for ax-addcl 8275, for naming consistency with addcli 8330. Use this theorem instead of ax-addcl 8275 or axaddcl 8231. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
addcl	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

Proof of Theorem addcl

Step	Hyp	Ref	Expression
1		ax-addcl 8275	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6085   CCcc 8177   + caddc 8182

This proof depends on axioms:  ax-addcl 8275

This theorem is used by:  adddir  8317  0cn  8318  addcli  8330  addcld  8345  muladd11  8460  peano2cn  8462  muladd11r  8483  add4  8488  cnegexlem3  8504  cnegex  8505  0cnALT  8517  negeu  8518  pncan  8533  2addsub  8541  addsubeq4  8542  nppcan2  8558  ppncan  8569  muladd  8712  mulsub  8729  recexap  8983  muleqadd  9000  conjmulap  9061  ofnegsub  9294  halfaddsubcl  9542  halfaddsub  9543  serf  10933  ser3add  10972  ser3sub  10973  ser0  10983  binom2  11101  binom3  11107  bernneq  11111  lswccatn0lsw  11393  shftlem  11595  shftval2  11605  shftval5  11608  2shfti  11610  crre  11636  crim  11637  cjadd  11663  addcj  11670  sqabsadd  11835  absreimsq  11847  absreim  11848  abstri  11885  addcn2  12092  climadd  12108  clim2ser  12119  clim2ser2  12120  isermulc2  12122  serf0  12134  sumrbdclem  12160  fsum3cvg  12161  summodclem3  12163  summodclem2a  12164  zsumdc  12167  fsum3  12170  fsum3cvg2  12177  fsum3ser  12180  fsumcl2lem  12181  fsumcl  12183  sumsnf  12192  fsummulc2  12231  binom  12267  isumshft  12273  isumsplit  12274  geolim2  12295  cvgratnnlemseq  12309  cvgratz  12315  ef0lem  12443  efcj  12456  ef4p  12477  efgt1p  12479  tanval3ap  12497  efi4p  12500  sinadd  12519  cosadd  12520  tanaddap  12522  addsin  12525  demoivreALT  12557  opoe  12678  pythagtriplem4  13067  pythagtriplem12  13074  gzaddcl  13176  cncrng  14955  addccncf  15750  dvaddxxbr  15851  dvaddxx  15853  dviaddf  15855  dveflem  15876  plyaddcl  15904  plymulcl  15905  plysubcl  15906  sinperlem  15959  ptolemy  15975  tangtx  15989  sinkpi  15998  binom4  16138  lgsquad2lem1  16298  2sqlem2  16332