Theorem addcl 7098

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

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1433  (class class class)co 5532   CCcc 6979   + caddc 6984

This theorem was proved from axioms:  ax-addcl 7072

This theorem is referenced by:  adddir  7110  0cn  7111  addcli  7123  addcld  7138  muladd11  7241  peano2cn  7243  muladd11r  7264  add4  7269  cnegexlem3  7285  cnegex  7286  0cnALT  7298  negeu  7299  pncan  7314  2addsub  7322  addsubeq4  7323  nppcan2  7339  ppncan  7350  muladd  7488  mulsub  7505  recexap  7743  muleqadd  7758  conjmulap  7817  halfaddsubcl  8264  halfaddsub  8265  iserf  9453  iseradd  9463  isersub  9464  iser0  9471  iser0f  9472  serige0  9473  serile  9474  binom2  9585  binom3  9590  bernneq  9593  shftlem  9704  shftval2  9714  shftval5  9717  2shfti  9719  crre  9744  crim  9745  cjadd  9771  addcj  9778  sqabsadd  9941  absreimsq  9953  absreim  9954  abstri  9990  addcn2  10149  climadd  10164  clim2iser  10175  clim2iser2  10176  iisermulc2  10178  iserile  10180  climserile  10183  serif0  10189  opoe  10295