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  10745  ser3add  10784  ser3sub  10785  ser0  10795  binom2  10913  binom3  10919  bernneq  10922  lswccatn0lsw  11188  shftlem  11377  shftval2  11387  shftval5  11390  2shfti  11392  crre  11418  crim  11419  cjadd  11445  addcj  11452  sqabsadd  11616  absreimsq  11628  absreim  11629  abstri  11665  addcn2  11871  climadd  11887  clim2ser  11898  clim2ser2  11899  isermulc2  11901  serf0  11913  sumrbdclem  11939  fsum3cvg  11940  summodclem3  11942  summodclem2a  11943  zsumdc  11946  fsum3  11949  fsum3cvg2  11956  fsum3ser  11959  fsumcl2lem  11960  fsumcl  11962  sumsnf  11971  fsummulc2  12010  binom  12046  isumshft  12052  isumsplit  12053  geolim2  12074  cvgratnnlemseq  12088  cvgratz  12094  ef0lem  12222  efcj  12235  ef4p  12256  efgt1p  12258  tanval3ap  12276  efi4p  12279  sinadd  12298  cosadd  12299  tanaddap  12301  addsin  12304  demoivreALT  12336  opoe  12457  pythagtriplem4  12842  pythagtriplem12  12849  gzaddcl  12951  cncrng  14585  addccncf  15326  dvaddxxbr  15427  dvaddxx  15429  dviaddf  15431  dveflem  15452  plyaddcl  15480  plymulcl  15481  plysubcl  15482  sinperlem  15534  ptolemy  15550  tangtx  15564  sinkpi  15573  binom4  15705  lgsquad2lem1  15812  2sqlem2  15846