Theorem addcl 7738

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480  (class class class)co 5767   CCcc 7611   + caddc 7616

This theorem was proved from axioms:  ax-addcl 7709

This theorem is referenced by:  adddir  7750  0cn  7751  addcli  7763  addcld  7778  muladd11  7888  peano2cn  7890  muladd11r  7911  add4  7916  cnegexlem3  7932  cnegex  7933  0cnALT  7945  negeu  7946  pncan  7961  2addsub  7969  addsubeq4  7970  nppcan2  7986  ppncan  7997  muladd  8139  mulsub  8156  recexap  8407  muleqadd  8422  conjmulap  8482  halfaddsubcl  8946  halfaddsub  8947  serf  10240  ser3add  10271  ser3sub  10272  ser0  10280  binom2  10396  binom3  10402  bernneq  10405  shftlem  10581  shftval2  10591  shftval5  10594  2shfti  10596  crre  10622  crim  10623  cjadd  10649  addcj  10656  sqabsadd  10820  absreimsq  10832  absreim  10833  abstri  10869  addcn2  11072  climadd  11088  clim2ser  11099  clim2ser2  11100  isermulc2  11102  serf0  11114  sumrbdclem  11138  fsum3cvg  11139  summodclem3  11142  summodclem2a  11143  zsumdc  11146  fsum3  11149  fsum3cvg2  11156  fsum3ser  11159  fsumcl2lem  11160  fsumcl  11162  sumsnf  11171  fsummulc2  11210  binom  11246  isumshft  11252  isumsplit  11253  geolim2  11274  cvgratnnlemseq  11288  cvgratz  11294  ef0lem  11355  efcj  11368  ef4p  11389  efgt1p  11391  tanval3ap  11410  efi4p  11413  sinadd  11432  cosadd  11433  tanaddap  11435  addsin  11438  demoivreALT  11469  opoe  11581  addccncf  12744  dvaddxxbr  12823  dvaddxx  12825  dviaddf  12827  dveflem  12844  sinperlem  12878  ptolemy  12894  tangtx  12908  sinkpi  12917