Theorem addcl 7745

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  (class class class)co 5774  ℂcc 7618   + caddc 7623

This theorem was proved from axioms:  ax-addcl 7716

This theorem is referenced by:  adddir  7757  0cn  7758  addcli  7770  addcld  7785  muladd11  7895  peano2cn  7897  muladd11r  7918  add4  7923  cnegexlem3  7939  cnegex  7940  0cnALT  7952  negeu  7953  pncan  7968  2addsub  7976  addsubeq4  7977  nppcan2  7993  ppncan  8004  muladd  8146  mulsub  8163  recexap  8414  muleqadd  8429  conjmulap  8489  halfaddsubcl  8953  halfaddsub  8954  serf  10247  ser3add  10278  ser3sub  10279  ser0  10287  binom2  10403  binom3  10409  bernneq  10412  shftlem  10588  shftval2  10598  shftval5  10601  2shfti  10603  crre  10629  crim  10630  cjadd  10656  addcj  10663  sqabsadd  10827  absreimsq  10839  absreim  10840  abstri  10876  addcn2  11079  climadd  11095  clim2ser  11106  clim2ser2  11107  isermulc2  11109  serf0  11121  sumrbdclem  11146  fsum3cvg  11147  summodclem3  11149  summodclem2a  11150  zsumdc  11153  fsum3  11156  fsum3cvg2  11163  fsum3ser  11166  fsumcl2lem  11167  fsumcl  11169  sumsnf  11178  fsummulc2  11217  binom  11253  isumshft  11259  isumsplit  11260  geolim2  11281  cvgratnnlemseq  11295  cvgratz  11301  ef0lem  11366  efcj  11379  ef4p  11400  efgt1p  11402  tanval3ap  11421  efi4p  11424  sinadd  11443  cosadd  11444  tanaddap  11446  addsin  11449  demoivreALT  11480  opoe  11592  addccncf  12755  dvaddxxbr  12834  dvaddxx  12836  dviaddf  12838  dveflem  12855  sinperlem  12889  ptolemy  12905  tangtx  12919  sinkpi  12928