Theorem addcl 8268

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2205  (class class class)co 6058   CCcc 8141   + caddc 8146

This theorem was proved from axioms:  ax-addcl 8239

This theorem is referenced by:  adddir  8281  0cn  8282  addcli  8294  addcld  8309  muladd11  8422  peano2cn  8424  muladd11r  8445  add4  8450  cnegexlem3  8466  cnegex  8467  0cnALT  8479  negeu  8480  pncan  8495  2addsub  8503  addsubeq4  8504  nppcan2  8520  ppncan  8531  muladd  8674  mulsub  8691  recexap  8944  muleqadd  8959  conjmulap  9020  ofnegsub  9253  halfaddsubcl  9488  halfaddsub  9489  serf  10869  ser3add  10908  ser3sub  10909  ser0  10919  binom2  11037  binom3  11043  bernneq  11047  lswccatn0lsw  11324  shftlem  11526  shftval2  11536  shftval5  11539  2shfti  11541  crre  11567  crim  11568  cjadd  11594  addcj  11601  sqabsadd  11765  absreimsq  11777  absreim  11778  abstri  11814  addcn2  12020  climadd  12036  clim2ser  12047  clim2ser2  12048  isermulc2  12050  serf0  12062  sumrbdclem  12088  fsum3cvg  12089  summodclem3  12091  summodclem2a  12092  zsumdc  12095  fsum3  12098  fsum3cvg2  12105  fsum3ser  12108  fsumcl2lem  12109  fsumcl  12111  sumsnf  12120  fsummulc2  12159  binom  12195  isumshft  12201  isumsplit  12202  geolim2  12223  cvgratnnlemseq  12237  cvgratz  12243  ef0lem  12371  efcj  12384  ef4p  12405  efgt1p  12407  tanval3ap  12425  efi4p  12428  sinadd  12447  cosadd  12448  tanaddap  12450  addsin  12453  demoivreALT  12485  opoe  12606  pythagtriplem4  12991  pythagtriplem12  12998  gzaddcl  13100  cncrng  14843  addccncf  15591  dvaddxxbr  15692  dvaddxx  15694  dviaddf  15696  dveflem  15717  plyaddcl  15745  plymulcl  15746  plysubcl  15747  sinperlem  15799  ptolemy  15815  tangtx  15829  sinkpi  15838  binom4  15970  lgsquad2lem1  16080  2sqlem2  16114