Theorem addcl 8310

Description: Alias for ax-addcl 8281, for naming consistency with addcli 8336. Use this theorem instead of ax-addcl 8281 or axaddcl 8237. (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 8281	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 6088   CCcc 8183   + caddc 8188

This proof depends on axioms:  ax-addcl 8281

This theorem is used by:  adddir  8323  0cn  8324  addcli  8336  addcld  8351  muladd11  8466  peano2cn  8468  muladd11r  8489  add4  8494  cnegexlem3  8510  cnegex  8511  0cnALT  8523  negeu  8524  pncan  8539  2addsub  8547  addsubeq4  8548  nppcan2  8564  ppncan  8575  muladd  8718  mulsub  8735  recexap  8989  muleqadd  9006  conjmulap  9067  ofnegsub  9301  halfaddsubcl  9549  halfaddsub  9550  serf  10941  ser3add  10980  ser3sub  10981  ser0  10991  binom2  11109  binom3  11115  bernneq  11119  lswccatn0lsw  11401  shftlem  11603  shftval2  11613  shftval5  11616  2shfti  11618  crre  11644  crim  11645  cjadd  11671  addcj  11678  sqabsadd  11843  absreimsq  11855  absreim  11856  abstri  11893  addcn2  12101  climadd  12117  clim2ser  12128  clim2ser2  12129  isermulc2  12131  serf0  12143  sumrbdclem  12169  fsum3cvg  12170  summodclem3  12172  summodclem2a  12173  zsumdc  12176  fsum3  12179  fsum3cvg2  12186  fsum3ser  12189  fsumcl2lem  12190  fsumcl  12192  sumsnf  12201  fsummulc2  12240  binom  12276  isumshft  12282  isumsplit  12283  geolim2  12304  cvgratnnlemseq  12318  cvgratz  12324  ef0lem  12452  efcj  12465  ef4p  12486  efgt1p  12488  tanval3ap  12506  efi4p  12509  sinadd  12528  cosadd  12529  tanaddap  12531  addsin  12534  demoivreALT  12566  opoe  12687  pythagtriplem4  13076  pythagtriplem12  13083  gzaddcl  13185  cncrng  15015  addccncf  15826  dvaddxxbr  15927  dvaddxx  15929  dviaddf  15931  dveflem  15952  plyaddcl  15980  plymulcl  15981  plysubcl  15982  sinperlem  16035  ptolemy  16051  tangtx  16065  sinkpi  16074  binom4  16219  prmorcht  16282  bposlem9  16319  lgsquad2lem1  16405  2sqlem2  16439