Theorem addcl 8294

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6075   CCcc 8167   + caddc 8172

This theorem was proved from axioms:  ax-addcl 8265

This theorem is referenced by:  adddir  8307  0cn  8308  addcli  8320  addcld  8335  muladd11  8449  peano2cn  8451  muladd11r  8472  add4  8477  cnegexlem3  8493  cnegex  8494  0cnALT  8506  negeu  8507  pncan  8522  2addsub  8530  addsubeq4  8531  nppcan2  8547  ppncan  8558  muladd  8701  mulsub  8718  recexap  8971  muleqadd  8988  conjmulap  9049  ofnegsub  9282  halfaddsubcl  9517  halfaddsub  9518  serf  10898  ser3add  10937  ser3sub  10938  ser0  10948  binom2  11066  binom3  11072  bernneq  11076  lswccatn0lsw  11357  shftlem  11559  shftval2  11569  shftval5  11572  2shfti  11574  crre  11600  crim  11601  cjadd  11627  addcj  11634  sqabsadd  11799  absreimsq  11811  absreim  11812  abstri  11848  addcn2  12054  climadd  12070  clim2ser  12081  clim2ser2  12082  isermulc2  12084  serf0  12096  sumrbdclem  12122  fsum3cvg  12123  summodclem3  12125  summodclem2a  12126  zsumdc  12129  fsum3  12132  fsum3cvg2  12139  fsum3ser  12142  fsumcl2lem  12143  fsumcl  12145  sumsnf  12154  fsummulc2  12193  binom  12229  isumshft  12235  isumsplit  12236  geolim2  12257  cvgratnnlemseq  12271  cvgratz  12277  ef0lem  12405  efcj  12418  ef4p  12439  efgt1p  12441  tanval3ap  12459  efi4p  12462  sinadd  12481  cosadd  12482  tanaddap  12484  addsin  12487  demoivreALT  12519  opoe  12640  pythagtriplem4  13025  pythagtriplem12  13032  gzaddcl  13134  cncrng  14878  addccncf  15624  dvaddxxbr  15725  dvaddxx  15727  dviaddf  15729  dveflem  15750  plyaddcl  15778  plymulcl  15779  plysubcl  15780  sinperlem  15832  ptolemy  15848  tangtx  15862  sinkpi  15871  binom4  16004  lgsquad2lem1  16114  2sqlem2  16148