Theorem addcl 8140

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   + caddc 8018

This theorem was proved from axioms:  ax-addcl 8111

This theorem is referenced by:  adddir  8153  0cn  8154  addcli  8166  addcld  8182  muladd11  8295  peano2cn  8297  muladd11r  8318  add4  8323  cnegexlem3  8339  cnegex  8340  0cnALT  8352  negeu  8353  pncan  8368  2addsub  8376  addsubeq4  8377  nppcan2  8393  ppncan  8404  muladd  8546  mulsub  8563  recexap  8816  muleqadd  8831  conjmulap  8892  ofnegsub  9125  halfaddsubcl  9360  halfaddsub  9361  serf  10722  ser3add  10761  ser3sub  10762  ser0  10772  binom2  10890  binom3  10896  bernneq  10899  lswccatn0lsw  11164  shftlem  11348  shftval2  11358  shftval5  11361  2shfti  11363  crre  11389  crim  11390  cjadd  11416  addcj  11423  sqabsadd  11587  absreimsq  11599  absreim  11600  abstri  11636  addcn2  11842  climadd  11858  clim2ser  11869  clim2ser2  11870  isermulc2  11872  serf0  11884  sumrbdclem  11909  fsum3cvg  11910  summodclem3  11912  summodclem2a  11913  zsumdc  11916  fsum3  11919  fsum3cvg2  11926  fsum3ser  11929  fsumcl2lem  11930  fsumcl  11932  sumsnf  11941  fsummulc2  11980  binom  12016  isumshft  12022  isumsplit  12023  geolim2  12044  cvgratnnlemseq  12058  cvgratz  12064  ef0lem  12192  efcj  12205  ef4p  12226  efgt1p  12228  tanval3ap  12246  efi4p  12249  sinadd  12268  cosadd  12269  tanaddap  12271  addsin  12274  demoivreALT  12306  opoe  12427  pythagtriplem4  12812  pythagtriplem12  12819  gzaddcl  12921  cncrng  14554  addccncf  15295  dvaddxxbr  15396  dvaddxx  15398  dviaddf  15400  dveflem  15421  plyaddcl  15449  plymulcl  15450  plysubcl  15451  sinperlem  15503  ptolemy  15519  tangtx  15533  sinkpi  15542  binom4  15674  lgsquad2lem1  15781  2sqlem2  15815