Theorem addcl 8150

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   + caddc 8028

This theorem was proved from axioms:  ax-addcl 8121

This theorem is referenced by:  adddir  8163  0cn  8164  addcli  8176  addcld  8192  muladd11  8305  peano2cn  8307  muladd11r  8328  add4  8333  cnegexlem3  8349  cnegex  8350  0cnALT  8362  negeu  8363  pncan  8378  2addsub  8386  addsubeq4  8387  nppcan2  8403  ppncan  8414  muladd  8556  mulsub  8573  recexap  8826  muleqadd  8841  conjmulap  8902  ofnegsub  9135  halfaddsubcl  9370  halfaddsub  9371  serf  10738  ser3add  10777  ser3sub  10778  ser0  10788  binom2  10906  binom3  10912  bernneq  10915  lswccatn0lsw  11181  shftlem  11370  shftval2  11380  shftval5  11383  2shfti  11385  crre  11411  crim  11412  cjadd  11438  addcj  11445  sqabsadd  11609  absreimsq  11621  absreim  11622  abstri  11658  addcn2  11864  climadd  11880  clim2ser  11891  clim2ser2  11892  isermulc2  11894  serf0  11906  sumrbdclem  11931  fsum3cvg  11932  summodclem3  11934  summodclem2a  11935  zsumdc  11938  fsum3  11941  fsum3cvg2  11948  fsum3ser  11951  fsumcl2lem  11952  fsumcl  11954  sumsnf  11963  fsummulc2  12002  binom  12038  isumshft  12044  isumsplit  12045  geolim2  12066  cvgratnnlemseq  12080  cvgratz  12086  ef0lem  12214  efcj  12227  ef4p  12248  efgt1p  12250  tanval3ap  12268  efi4p  12271  sinadd  12290  cosadd  12291  tanaddap  12293  addsin  12296  demoivreALT  12328  opoe  12449  pythagtriplem4  12834  pythagtriplem12  12841  gzaddcl  12943  cncrng  14576  addccncf  15317  dvaddxxbr  15418  dvaddxx  15420  dviaddf  15422  dveflem  15443  plyaddcl  15471  plymulcl  15472  plysubcl  15473  sinperlem  15525  ptolemy  15541  tangtx  15555  sinkpi  15564  binom4  15696  lgsquad2lem1  15803  2sqlem2  15837