Theorem addcl 8157

Description: Alias for ax-addcl 8128, for naming consistency with addcli 8183. Use this theorem instead of ax-addcl 8128 or axaddcl 8084. (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 8128	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202  (class class class)co 6018   CCcc 8030   + caddc 8035

This theorem was proved from axioms:  ax-addcl 8128

This theorem is referenced by:  adddir  8170  0cn  8171  addcli  8183  addcld  8199  muladd11  8312  peano2cn  8314  muladd11r  8335  add4  8340  cnegexlem3  8356  cnegex  8357  0cnALT  8369  negeu  8370  pncan  8385  2addsub  8393  addsubeq4  8394  nppcan2  8410  ppncan  8421  muladd  8563  mulsub  8580  recexap  8833  muleqadd  8848  conjmulap  8909  ofnegsub  9142  halfaddsubcl  9377  halfaddsub  9378  serf  10746  ser3add  10785  ser3sub  10786  ser0  10796  binom2  10914  binom3  10920  bernneq  10923  lswccatn0lsw  11192  shftlem  11381  shftval2  11391  shftval5  11394  2shfti  11396  crre  11422  crim  11423  cjadd  11449  addcj  11456  sqabsadd  11620  absreimsq  11632  absreim  11633  abstri  11669  addcn2  11875  climadd  11891  clim2ser  11902  clim2ser2  11903  isermulc2  11905  serf0  11917  sumrbdclem  11943  fsum3cvg  11944  summodclem3  11946  summodclem2a  11947  zsumdc  11950  fsum3  11953  fsum3cvg2  11960  fsum3ser  11963  fsumcl2lem  11964  fsumcl  11966  sumsnf  11975  fsummulc2  12014  binom  12050  isumshft  12056  isumsplit  12057  geolim2  12078  cvgratnnlemseq  12092  cvgratz  12098  ef0lem  12226  efcj  12239  ef4p  12260  efgt1p  12262  tanval3ap  12280  efi4p  12283  sinadd  12302  cosadd  12303  tanaddap  12305  addsin  12308  demoivreALT  12340  opoe  12461  pythagtriplem4  12846  pythagtriplem12  12853  gzaddcl  12955  cncrng  14589  addccncf  15330  dvaddxxbr  15431  dvaddxx  15433  dviaddf  15435  dveflem  15456  plyaddcl  15484  plymulcl  15485  plysubcl  15486  sinperlem  15538  ptolemy  15554  tangtx  15568  sinkpi  15577  binom4  15709  lgsquad2lem1  15816  2sqlem2  15850