Theorem addcl 8156

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202  (class class class)co 6017   CCcc 8029   + caddc 8034

This theorem was proved from axioms:  ax-addcl 8127

This theorem is referenced by:  adddir  8169  0cn  8170  addcli  8182  addcld  8198  muladd11  8311  peano2cn  8313  muladd11r  8334  add4  8339  cnegexlem3  8355  cnegex  8356  0cnALT  8368  negeu  8369  pncan  8384  2addsub  8392  addsubeq4  8393  nppcan2  8409  ppncan  8420  muladd  8562  mulsub  8579  recexap  8832  muleqadd  8847  conjmulap  8908  ofnegsub  9141  halfaddsubcl  9376  halfaddsub  9377  serf  10744  ser3add  10783  ser3sub  10784  ser0  10794  binom2  10912  binom3  10918  bernneq  10921  lswccatn0lsw  11187  shftlem  11376  shftval2  11386  shftval5  11389  2shfti  11391  crre  11417  crim  11418  cjadd  11444  addcj  11451  sqabsadd  11615  absreimsq  11627  absreim  11628  abstri  11664  addcn2  11870  climadd  11886  clim2ser  11897  clim2ser2  11898  isermulc2  11900  serf0  11912  sumrbdclem  11937  fsum3cvg  11938  summodclem3  11940  summodclem2a  11941  zsumdc  11944  fsum3  11947  fsum3cvg2  11954  fsum3ser  11957  fsumcl2lem  11958  fsumcl  11960  sumsnf  11969  fsummulc2  12008  binom  12044  isumshft  12050  isumsplit  12051  geolim2  12072  cvgratnnlemseq  12086  cvgratz  12092  ef0lem  12220  efcj  12233  ef4p  12254  efgt1p  12256  tanval3ap  12274  efi4p  12277  sinadd  12296  cosadd  12297  tanaddap  12299  addsin  12302  demoivreALT  12334  opoe  12455  pythagtriplem4  12840  pythagtriplem12  12847  gzaddcl  12949  cncrng  14582  addccncf  15323  dvaddxxbr  15424  dvaddxx  15426  dviaddf  15428  dveflem  15449  plyaddcl  15477  plymulcl  15478  plysubcl  15479  sinperlem  15531  ptolemy  15547  tangtx  15561  sinkpi  15570  binom4  15702  lgsquad2lem1  15809  2sqlem2  15843