Theorem addcl 7006

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

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1393  (class class class)co 5512   CCcc 6887   + caddc 6892

This theorem was proved from axioms:  ax-addcl 6980

This theorem is referenced by:  adddir  7018  0cn  7019  addcli  7031  addcld  7046  muladd11  7146  peano2cn  7148  add4  7172  cnegexlem3  7188  cnegex  7189  0cnALT  7201  negeu  7202  pncan  7217  2addsub  7225  addsubeq4  7226  nppcan2  7242  ppncan  7253  muladd  7381  mulsub  7398  recexap  7634  muleqadd  7649  conjmulap  7705  halfaddsubcl  8158  halfaddsub  8159  iserf  9233  iseradd  9243  isersub  9244  iser0  9250  iser0f  9251  serige0  9252  serile  9253  binom2  9362  binom3  9366  bernneq  9369  shftlem  9417  shftval2  9427  shftval5  9430  2shfti  9432  crre  9457  crim  9458  cjadd  9484  addcj  9491  sqabsadd  9653  absreimsq  9665  absreim  9666  abstri  9700  addcn2  9831  climadd  9846  clim2iser  9857  clim2iser2  9858  iisermulc2  9860  iserile  9862  climserile  9865  serif0  9871