Theorem addcl 7149

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1434  (class class class)co 5537  ℂcc 7030   + caddc 7035

This theorem was proved from axioms:  ax-addcl 7123

This theorem is referenced by:  adddir  7161  0cn  7162  addcli  7174  addcld  7189  muladd11  7297  peano2cn  7299  muladd11r  7320  add4  7325  cnegexlem3  7341  cnegex  7342  0cnALT  7354  negeu  7355  pncan  7370  2addsub  7378  addsubeq4  7379  nppcan2  7395  ppncan  7406  muladd  7544  mulsub  7561  recexap  7799  muleqadd  7814  conjmulap  7873  halfaddsubcl  8320  halfaddsub  8321  iserf  9538  iseradd  9548  isersub  9549  iser0  9557  serige0  9559  serile  9560  binom2  9671  binom3  9676  bernneq  9679  shftlem  9831  shftval2  9841  shftval5  9844  2shfti  9846  crre  9871  crim  9872  cjadd  9898  addcj  9905  sqabsadd  10068  absreimsq  10080  absreim  10081  abstri  10117  addcn2  10276  climadd  10291  clim2iser  10302  clim2iser2  10303  iisermulc2  10305  iserile  10307  climserile  10310  serif0  10316  isumrblem  10326  fisumcvg  10327  opoe  10428