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  10940  ser3add  10979  ser3sub  10980  ser0  10990  binom2  11108  binom3  11114  bernneq  11118  lswccatn0lsw  11400  shftlem  11602  shftval2  11612  shftval5  11615  2shfti  11617  crre  11643  crim  11644  cjadd  11670  addcj  11677  sqabsadd  11842  absreimsq  11854  absreim  11855  abstri  11892  addcn2  12100  climadd  12116  clim2ser  12127  clim2ser2  12128  isermulc2  12130  serf0  12142  sumrbdclem  12168  fsum3cvg  12169  summodclem3  12171  summodclem2a  12172  zsumdc  12175  fsum3  12178  fsum3cvg2  12185  fsum3ser  12188  fsumcl2lem  12189  fsumcl  12191  sumsnf  12200  fsummulc2  12239  binom  12275  isumshft  12281  isumsplit  12282  geolim2  12303  cvgratnnlemseq  12317  cvgratz  12323  ef0lem  12451  efcj  12464  ef4p  12485  efgt1p  12487  tanval3ap  12505  efi4p  12508  sinadd  12527  cosadd  12528  tanaddap  12530  addsin  12533  demoivreALT  12565  opoe  12686  pythagtriplem4  13075  pythagtriplem12  13082  gzaddcl  13184  cncrng  15014  addccncf  15843  dvaddxxbr  15944  dvaddxx  15946  dviaddf  15948  dveflem  15969  plyaddcl  15997  plymulcl  15998  plysubcl  15999  sinperlem  16052  ptolemy  16068  tangtx  16082  sinkpi  16091  binom4  16236  prmorcht  16299  bposlem9  16336  lgsquad2lem1  16422  2sqlem2  16456