Theorem addcl 8023

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   + caddc 7901

This theorem was proved from axioms:  ax-addcl 7994

This theorem is referenced by:  adddir  8036  0cn  8037  addcli  8049  addcld  8065  muladd11  8178  peano2cn  8180  muladd11r  8201  add4  8206  cnegexlem3  8222  cnegex  8223  0cnALT  8235  negeu  8236  pncan  8251  2addsub  8259  addsubeq4  8260  nppcan2  8276  ppncan  8287  muladd  8429  mulsub  8446  recexap  8699  muleqadd  8714  conjmulap  8775  ofnegsub  9008  halfaddsubcl  9243  halfaddsub  9244  serf  10594  ser3add  10633  ser3sub  10634  ser0  10644  binom2  10762  binom3  10768  bernneq  10771  shftlem  11000  shftval2  11010  shftval5  11013  2shfti  11015  crre  11041  crim  11042  cjadd  11068  addcj  11075  sqabsadd  11239  absreimsq  11251  absreim  11252  abstri  11288  addcn2  11494  climadd  11510  clim2ser  11521  clim2ser2  11522  isermulc2  11524  serf0  11536  sumrbdclem  11561  fsum3cvg  11562  summodclem3  11564  summodclem2a  11565  zsumdc  11568  fsum3  11571  fsum3cvg2  11578  fsum3ser  11581  fsumcl2lem  11582  fsumcl  11584  sumsnf  11593  fsummulc2  11632  binom  11668  isumshft  11674  isumsplit  11675  geolim2  11696  cvgratnnlemseq  11710  cvgratz  11716  ef0lem  11844  efcj  11857  ef4p  11878  efgt1p  11880  tanval3ap  11898  efi4p  11901  sinadd  11920  cosadd  11921  tanaddap  11923  addsin  11926  demoivreALT  11958  opoe  12079  pythagtriplem4  12464  pythagtriplem12  12471  gzaddcl  12573  cncrng  14203  addccncf  14922  dvaddxxbr  15023  dvaddxx  15025  dviaddf  15027  dveflem  15048  plyaddcl  15076  plymulcl  15077  plysubcl  15078  sinperlem  15130  ptolemy  15146  tangtx  15160  sinkpi  15169  binom4  15301  lgsquad2lem1  15408  2sqlem2  15442