Theorem addcl 7999

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2164  (class class class)co 5919   CCcc 7872   + caddc 7877

This theorem was proved from axioms:  ax-addcl 7970

This theorem is referenced by:  adddir  8012  0cn  8013  addcli  8025  addcld  8041  muladd11  8154  peano2cn  8156  muladd11r  8177  add4  8182  cnegexlem3  8198  cnegex  8199  0cnALT  8211  negeu  8212  pncan  8227  2addsub  8235  addsubeq4  8236  nppcan2  8252  ppncan  8263  muladd  8405  mulsub  8422  recexap  8674  muleqadd  8689  conjmulap  8750  ofnegsub  8983  halfaddsubcl  9218  halfaddsub  9219  serf  10557  ser3add  10596  ser3sub  10597  ser0  10607  binom2  10725  binom3  10731  bernneq  10734  shftlem  10963  shftval2  10973  shftval5  10976  2shfti  10978  crre  11004  crim  11005  cjadd  11031  addcj  11038  sqabsadd  11202  absreimsq  11214  absreim  11215  abstri  11251  addcn2  11456  climadd  11472  clim2ser  11483  clim2ser2  11484  isermulc2  11486  serf0  11498  sumrbdclem  11523  fsum3cvg  11524  summodclem3  11526  summodclem2a  11527  zsumdc  11530  fsum3  11533  fsum3cvg2  11540  fsum3ser  11543  fsumcl2lem  11544  fsumcl  11546  sumsnf  11555  fsummulc2  11594  binom  11630  isumshft  11636  isumsplit  11637  geolim2  11658  cvgratnnlemseq  11672  cvgratz  11678  ef0lem  11806  efcj  11819  ef4p  11840  efgt1p  11842  tanval3ap  11860  efi4p  11863  sinadd  11882  cosadd  11883  tanaddap  11885  addsin  11888  demoivreALT  11920  opoe  12039  pythagtriplem4  12409  pythagtriplem12  12416  gzaddcl  12518  cncrng  14068  addccncf  14779  dvaddxxbr  14880  dvaddxx  14882  dviaddf  14884  dveflem  14905  plyaddcl  14933  plymulcl  14934  plysubcl  14935  sinperlem  14984  ptolemy  15000  tangtx  15014  sinkpi  15023  binom4  15152  lgsquad2lem1  15238  2sqlem2  15272