Theorem addcl 7769

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1481  (class class class)co 5782   CCcc 7642   + caddc 7647

This theorem was proved from axioms:  ax-addcl 7740

This theorem is referenced by:  adddir  7781  0cn  7782  addcli  7794  addcld  7809  muladd11  7919  peano2cn  7921  muladd11r  7942  add4  7947  cnegexlem3  7963  cnegex  7964  0cnALT  7976  negeu  7977  pncan  7992  2addsub  8000  addsubeq4  8001  nppcan2  8017  ppncan  8028  muladd  8170  mulsub  8187  recexap  8438  muleqadd  8453  conjmulap  8513  halfaddsubcl  8977  halfaddsub  8978  serf  10278  ser3add  10309  ser3sub  10310  ser0  10318  binom2  10434  binom3  10440  bernneq  10443  shftlem  10620  shftval2  10630  shftval5  10633  2shfti  10635  crre  10661  crim  10662  cjadd  10688  addcj  10695  sqabsadd  10859  absreimsq  10871  absreim  10872  abstri  10908  addcn2  11111  climadd  11127  clim2ser  11138  clim2ser2  11139  isermulc2  11141  serf0  11153  sumrbdclem  11178  fsum3cvg  11179  summodclem3  11181  summodclem2a  11182  zsumdc  11185  fsum3  11188  fsum3cvg2  11195  fsum3ser  11198  fsumcl2lem  11199  fsumcl  11201  sumsnf  11210  fsummulc2  11249  binom  11285  isumshft  11291  isumsplit  11292  geolim2  11313  cvgratnnlemseq  11327  cvgratz  11333  ef0lem  11403  efcj  11416  ef4p  11437  efgt1p  11439  tanval3ap  11457  efi4p  11460  sinadd  11479  cosadd  11480  tanaddap  11482  addsin  11485  demoivreALT  11516  opoe  11628  addccncf  12794  dvaddxxbr  12873  dvaddxx  12875  dviaddf  12877  dveflem  12895  sinperlem  12937  ptolemy  12953  tangtx  12967  sinkpi  12976