Theorem addcl 8305

Description: Alias for ax-addcl 8276, for naming consistency with addcli 8331. Use this theorem instead of ax-addcl 8276 or axaddcl 8232. (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 8276	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 8178   + caddc 8183

This proof depends on axioms:  ax-addcl 8276

This theorem is used by:  adddir  8318  0cn  8319  addcli  8331  addcld  8346  muladd11  8461  peano2cn  8463  muladd11r  8484  add4  8489  cnegexlem3  8505  cnegex  8506  0cnALT  8518  negeu  8519  pncan  8534  2addsub  8542  addsubeq4  8543  nppcan2  8559  ppncan  8570  muladd  8713  mulsub  8730  recexap  8984  muleqadd  9001  conjmulap  9062  ofnegsub  9295  halfaddsubcl  9543  halfaddsub  9544  serf  10935  ser3add  10974  ser3sub  10975  ser0  10985  binom2  11103  binom3  11109  bernneq  11113  lswccatn0lsw  11395  shftlem  11597  shftval2  11607  shftval5  11610  2shfti  11612  crre  11638  crim  11639  cjadd  11665  addcj  11672  sqabsadd  11837  absreimsq  11849  absreim  11850  abstri  11887  addcn2  12095  climadd  12111  clim2ser  12122  clim2ser2  12123  isermulc2  12125  serf0  12137  sumrbdclem  12163  fsum3cvg  12164  summodclem3  12166  summodclem2a  12167  zsumdc  12170  fsum3  12173  fsum3cvg2  12180  fsum3ser  12183  fsumcl2lem  12184  fsumcl  12186  sumsnf  12195  fsummulc2  12234  binom  12270  isumshft  12276  isumsplit  12277  geolim2  12298  cvgratnnlemseq  12312  cvgratz  12318  ef0lem  12446  efcj  12459  ef4p  12480  efgt1p  12482  tanval3ap  12500  efi4p  12503  sinadd  12522  cosadd  12523  tanaddap  12525  addsin  12528  demoivreALT  12560  opoe  12681  pythagtriplem4  13070  pythagtriplem12  13077  gzaddcl  13179  cncrng  14990  addccncf  15792  dvaddxxbr  15893  dvaddxx  15895  dviaddf  15897  dveflem  15918  plyaddcl  15946  plymulcl  15947  plysubcl  15948  sinperlem  16001  ptolemy  16017  tangtx  16031  sinkpi  16040  binom4  16180  prmorcht  16243  bposlem9  16280  lgsquad2lem1  16366  2sqlem2  16400