Theorem addcl 8304

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209  (class class class)co 6085   CCcc 8177   + caddc 8182

This proof depends on axioms:  ax-addcl 8275

This theorem is used by:  adddir  8317  0cn  8318  addcli  8330  addcld  8345  muladd11  8459  peano2cn  8461  muladd11r  8482  add4  8487  cnegexlem3  8503  cnegex  8504  0cnALT  8516  negeu  8517  pncan  8532  2addsub  8540  addsubeq4  8541  nppcan2  8557  ppncan  8568  muladd  8711  mulsub  8728  recexap  8981  muleqadd  8998  conjmulap  9059  ofnegsub  9292  halfaddsubcl  9538  halfaddsub  9539  serf  10920  ser3add  10959  ser3sub  10960  ser0  10970  binom2  11088  binom3  11094  bernneq  11098  lswccatn0lsw  11379  shftlem  11581  shftval2  11591  shftval5  11594  2shfti  11596  crre  11622  crim  11623  cjadd  11649  addcj  11656  sqabsadd  11821  absreimsq  11833  absreim  11834  abstri  11870  addcn2  12076  climadd  12092  clim2ser  12103  clim2ser2  12104  isermulc2  12106  serf0  12118  sumrbdclem  12144  fsum3cvg  12145  summodclem3  12147  summodclem2a  12148  zsumdc  12151  fsum3  12154  fsum3cvg2  12161  fsum3ser  12164  fsumcl2lem  12165  fsumcl  12167  sumsnf  12176  fsummulc2  12215  binom  12251  isumshft  12257  isumsplit  12258  geolim2  12279  cvgratnnlemseq  12293  cvgratz  12299  ef0lem  12427  efcj  12440  ef4p  12461  efgt1p  12463  tanval3ap  12481  efi4p  12484  sinadd  12503  cosadd  12504  tanaddap  12506  addsin  12509  demoivreALT  12541  opoe  12662  pythagtriplem4  13047  pythagtriplem12  13054  gzaddcl  13156  cncrng  14906  addccncf  15701  dvaddxxbr  15802  dvaddxx  15804  dviaddf  15806  dveflem  15827  plyaddcl  15855  plymulcl  15856  plysubcl  15857  sinperlem  15909  ptolemy  15925  tangtx  15939  sinkpi  15948  binom4  16081  lgsquad2lem1  16200  2sqlem2  16234