Theorem addcl 7935

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  (class class class)co 5874  ℂcc 7808   + caddc 7813

This theorem was proved from axioms:  ax-addcl 7906

This theorem is referenced by:  adddir  7947  0cn  7948  addcli  7960  addcld  7976  muladd11  8089  peano2cn  8091  muladd11r  8112  add4  8117  cnegexlem3  8133  cnegex  8134  0cnALT  8146  negeu  8147  pncan  8162  2addsub  8170  addsubeq4  8171  nppcan2  8187  ppncan  8198  muladd  8340  mulsub  8357  recexap  8609  muleqadd  8624  conjmulap  8685  halfaddsubcl  9151  halfaddsub  9152  serf  10473  ser3add  10504  ser3sub  10505  ser0  10513  binom2  10631  binom3  10637  bernneq  10640  shftlem  10824  shftval2  10834  shftval5  10837  2shfti  10839  crre  10865  crim  10866  cjadd  10892  addcj  10899  sqabsadd  11063  absreimsq  11075  absreim  11076  abstri  11112  addcn2  11317  climadd  11333  clim2ser  11344  clim2ser2  11345  isermulc2  11347  serf0  11359  sumrbdclem  11384  fsum3cvg  11385  summodclem3  11387  summodclem2a  11388  zsumdc  11391  fsum3  11394  fsum3cvg2  11401  fsum3ser  11404  fsumcl2lem  11405  fsumcl  11407  sumsnf  11416  fsummulc2  11455  binom  11491  isumshft  11497  isumsplit  11498  geolim2  11519  cvgratnnlemseq  11533  cvgratz  11539  ef0lem  11667  efcj  11680  ef4p  11701  efgt1p  11703  tanval3ap  11721  efi4p  11724  sinadd  11743  cosadd  11744  tanaddap  11746  addsin  11749  demoivreALT  11780  opoe  11899  pythagtriplem4  12267  pythagtriplem12  12274  gzaddcl  12374  cncrng  13433  addccncf  14056  dvaddxxbr  14135  dvaddxx  14137  dviaddf  14139  dveflem  14157  sinperlem  14199  ptolemy  14215  tangtx  14229  sinkpi  14238  binom4  14367  2sqlem2  14432