Theorem addcl 8132

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   + caddc 8010

This theorem was proved from axioms:  ax-addcl 8103

This theorem is referenced by:  adddir  8145  0cn  8146  addcli  8158  addcld  8174  muladd11  8287  peano2cn  8289  muladd11r  8310  add4  8315  cnegexlem3  8331  cnegex  8332  0cnALT  8344  negeu  8345  pncan  8360  2addsub  8368  addsubeq4  8369  nppcan2  8385  ppncan  8396  muladd  8538  mulsub  8555  recexap  8808  muleqadd  8823  conjmulap  8884  ofnegsub  9117  halfaddsubcl  9352  halfaddsub  9353  serf  10713  ser3add  10752  ser3sub  10753  ser0  10763  binom2  10881  binom3  10887  bernneq  10890  lswccatn0lsw  11154  shftlem  11335  shftval2  11345  shftval5  11348  2shfti  11350  crre  11376  crim  11377  cjadd  11403  addcj  11410  sqabsadd  11574  absreimsq  11586  absreim  11587  abstri  11623  addcn2  11829  climadd  11845  clim2ser  11856  clim2ser2  11857  isermulc2  11859  serf0  11871  sumrbdclem  11896  fsum3cvg  11897  summodclem3  11899  summodclem2a  11900  zsumdc  11903  fsum3  11906  fsum3cvg2  11913  fsum3ser  11916  fsumcl2lem  11917  fsumcl  11919  sumsnf  11928  fsummulc2  11967  binom  12003  isumshft  12009  isumsplit  12010  geolim2  12031  cvgratnnlemseq  12045  cvgratz  12051  ef0lem  12179  efcj  12192  ef4p  12213  efgt1p  12215  tanval3ap  12233  efi4p  12236  sinadd  12255  cosadd  12256  tanaddap  12258  addsin  12261  demoivreALT  12293  opoe  12414  pythagtriplem4  12799  pythagtriplem12  12806  gzaddcl  12908  cncrng  14541  addccncf  15282  dvaddxxbr  15383  dvaddxx  15385  dviaddf  15387  dveflem  15408  plyaddcl  15436  plymulcl  15437  plysubcl  15438  sinperlem  15490  ptolemy  15506  tangtx  15520  sinkpi  15529  binom4  15661  lgsquad2lem1  15768  2sqlem2  15802