Theorem addcl 8200

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202  (class class class)co 6028   CCcc 8073   + caddc 8078

This theorem was proved from axioms:  ax-addcl 8171

This theorem is referenced by:  adddir  8213  0cn  8214  addcli  8226  addcld  8241  muladd11  8354  peano2cn  8356  muladd11r  8377  add4  8382  cnegexlem3  8398  cnegex  8399  0cnALT  8411  negeu  8412  pncan  8427  2addsub  8435  addsubeq4  8436  nppcan2  8452  ppncan  8463  muladd  8605  mulsub  8622  recexap  8875  muleqadd  8890  conjmulap  8951  ofnegsub  9184  halfaddsubcl  9419  halfaddsub  9420  serf  10791  ser3add  10830  ser3sub  10831  ser0  10841  binom2  10959  binom3  10965  bernneq  10968  lswccatn0lsw  11237  shftlem  11439  shftval2  11449  shftval5  11452  2shfti  11454  crre  11480  crim  11481  cjadd  11507  addcj  11514  sqabsadd  11678  absreimsq  11690  absreim  11691  abstri  11727  addcn2  11933  climadd  11949  clim2ser  11960  clim2ser2  11961  isermulc2  11963  serf0  11975  sumrbdclem  12001  fsum3cvg  12002  summodclem3  12004  summodclem2a  12005  zsumdc  12008  fsum3  12011  fsum3cvg2  12018  fsum3ser  12021  fsumcl2lem  12022  fsumcl  12024  sumsnf  12033  fsummulc2  12072  binom  12108  isumshft  12114  isumsplit  12115  geolim2  12136  cvgratnnlemseq  12150  cvgratz  12156  ef0lem  12284  efcj  12297  ef4p  12318  efgt1p  12320  tanval3ap  12338  efi4p  12341  sinadd  12360  cosadd  12361  tanaddap  12363  addsin  12366  demoivreALT  12398  opoe  12519  pythagtriplem4  12904  pythagtriplem12  12911  gzaddcl  13013  cncrng  14648  addccncf  15394  dvaddxxbr  15495  dvaddxx  15497  dviaddf  15499  dveflem  15520  plyaddcl  15548  plymulcl  15549  plysubcl  15550  sinperlem  15602  ptolemy  15618  tangtx  15632  sinkpi  15641  binom4  15773  lgsquad2lem1  15883  2sqlem2  15917