Theorem addcl 8157

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   + caddc 8035

This theorem was proved from axioms:  ax-addcl 8128

This theorem is referenced by:  adddir  8170  0cn  8171  addcli  8183  addcld  8199  muladd11  8312  peano2cn  8314  muladd11r  8335  add4  8340  cnegexlem3  8356  cnegex  8357  0cnALT  8369  negeu  8370  pncan  8385  2addsub  8393  addsubeq4  8394  nppcan2  8410  ppncan  8421  muladd  8563  mulsub  8580  recexap  8833  muleqadd  8848  conjmulap  8909  ofnegsub  9142  halfaddsubcl  9377  halfaddsub  9378  serf  10746  ser3add  10785  ser3sub  10786  ser0  10796  binom2  10914  binom3  10920  bernneq  10923  lswccatn0lsw  11189  shftlem  11378  shftval2  11388  shftval5  11391  2shfti  11393  crre  11419  crim  11420  cjadd  11446  addcj  11453  sqabsadd  11617  absreimsq  11629  absreim  11630  abstri  11666  addcn2  11872  climadd  11888  clim2ser  11899  clim2ser2  11900  isermulc2  11902  serf0  11914  sumrbdclem  11940  fsum3cvg  11941  summodclem3  11943  summodclem2a  11944  zsumdc  11947  fsum3  11950  fsum3cvg2  11957  fsum3ser  11960  fsumcl2lem  11961  fsumcl  11963  sumsnf  11972  fsummulc2  12011  binom  12047  isumshft  12053  isumsplit  12054  geolim2  12075  cvgratnnlemseq  12089  cvgratz  12095  ef0lem  12223  efcj  12236  ef4p  12257  efgt1p  12259  tanval3ap  12277  efi4p  12280  sinadd  12299  cosadd  12300  tanaddap  12302  addsin  12305  demoivreALT  12337  opoe  12458  pythagtriplem4  12843  pythagtriplem12  12850  gzaddcl  12952  cncrng  14586  addccncf  15327  dvaddxxbr  15428  dvaddxx  15430  dviaddf  15432  dveflem  15453  plyaddcl  15481  plymulcl  15482  plysubcl  15483  sinperlem  15535  ptolemy  15551  tangtx  15565  sinkpi  15574  binom4  15706  lgsquad2lem1  15813  2sqlem2  15847