Theorem addcl 7004

Description: Alias for ax-addcl 6978, for naming consistency with addcli 7029. Use this theorem instead of ax-addcl 6978 or axaddcl 6938. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
addcl	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Proof of Theorem addcl

Step	Hyp	Ref	Expression
1		ax-addcl 6978	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 97   ∈ wcel 1393  (class class class)co 5512  ℂcc 6885   + caddc 6890

This theorem was proved from axioms:  ax-addcl 6978

This theorem is referenced by:  adddir  7016  0cn  7017  addcli  7029  addcld  7044  muladd11  7144  peano2cn  7146  add4  7170  cnegexlem3  7186  cnegex  7187  0cnALT  7199  negeu  7200  pncan  7215  2addsub  7223  addsubeq4  7224  nppcan2  7240  ppncan  7251  muladd  7379  mulsub  7396  recexap  7632  muleqadd  7647  conjmulap  7703  halfaddsubcl  8156  halfaddsub  8157  iserf  9207  iseradd  9217  isersub  9218  iser0  9224  iser0f  9225  serige0  9226  serile  9227  binom2  9336  binom3  9340  bernneq  9343  shftlem  9391  shftval2  9401  shftval5  9404  2shfti  9406  crre  9431  crim  9432  cjadd  9458  addcj  9465  sqabsadd  9627  absreimsq  9639  absreim  9640  abstri  9674  addcn2  9805  climadd  9820  clim2iser  9831  clim2iser2  9832  iisermulc2  9834  iserile  9836  climserile  9839  serif0  9845