Theorem addcl 8021

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2167  (class class class)co 5925   CCcc 7894   + caddc 7899

This theorem was proved from axioms:  ax-addcl 7992

This theorem is referenced by:  adddir  8034  0cn  8035  addcli  8047  addcld  8063  muladd11  8176  peano2cn  8178  muladd11r  8199  add4  8204  cnegexlem3  8220  cnegex  8221  0cnALT  8233  negeu  8234  pncan  8249  2addsub  8257  addsubeq4  8258  nppcan2  8274  ppncan  8285  muladd  8427  mulsub  8444  recexap  8697  muleqadd  8712  conjmulap  8773  ofnegsub  9006  halfaddsubcl  9241  halfaddsub  9242  serf  10592  ser3add  10631  ser3sub  10632  ser0  10642  binom2  10760  binom3  10766  bernneq  10769  shftlem  10998  shftval2  11008  shftval5  11011  2shfti  11013  crre  11039  crim  11040  cjadd  11066  addcj  11073  sqabsadd  11237  absreimsq  11249  absreim  11250  abstri  11286  addcn2  11492  climadd  11508  clim2ser  11519  clim2ser2  11520  isermulc2  11522  serf0  11534  sumrbdclem  11559  fsum3cvg  11560  summodclem3  11562  summodclem2a  11563  zsumdc  11566  fsum3  11569  fsum3cvg2  11576  fsum3ser  11579  fsumcl2lem  11580  fsumcl  11582  sumsnf  11591  fsummulc2  11630  binom  11666  isumshft  11672  isumsplit  11673  geolim2  11694  cvgratnnlemseq  11708  cvgratz  11714  ef0lem  11842  efcj  11855  ef4p  11876  efgt1p  11878  tanval3ap  11896  efi4p  11899  sinadd  11918  cosadd  11919  tanaddap  11921  addsin  11924  demoivreALT  11956  opoe  12077  pythagtriplem4  12462  pythagtriplem12  12469  gzaddcl  12571  cncrng  14201  addccncf  14920  dvaddxxbr  15021  dvaddxx  15023  dviaddf  15025  dveflem  15046  plyaddcl  15074  plymulcl  15075  plysubcl  15076  sinperlem  15128  ptolemy  15144  tangtx  15158  sinkpi  15167  binom4  15299  lgsquad2lem1  15406  2sqlem2  15440