Theorem addcl 7878

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136  (class class class)co 5842  ℂcc 7751   + caddc 7756

This theorem was proved from axioms:  ax-addcl 7849

This theorem is referenced by:  adddir  7890  0cn  7891  addcli  7903  addcld  7918  muladd11  8031  peano2cn  8033  muladd11r  8054  add4  8059  cnegexlem3  8075  cnegex  8076  0cnALT  8088  negeu  8089  pncan  8104  2addsub  8112  addsubeq4  8113  nppcan2  8129  ppncan  8140  muladd  8282  mulsub  8299  recexap  8550  muleqadd  8565  conjmulap  8625  halfaddsubcl  9090  halfaddsub  9091  serf  10409  ser3add  10440  ser3sub  10441  ser0  10449  binom2  10566  binom3  10572  bernneq  10575  shftlem  10758  shftval2  10768  shftval5  10771  2shfti  10773  crre  10799  crim  10800  cjadd  10826  addcj  10833  sqabsadd  10997  absreimsq  11009  absreim  11010  abstri  11046  addcn2  11251  climadd  11267  clim2ser  11278  clim2ser2  11279  isermulc2  11281  serf0  11293  sumrbdclem  11318  fsum3cvg  11319  summodclem3  11321  summodclem2a  11322  zsumdc  11325  fsum3  11328  fsum3cvg2  11335  fsum3ser  11338  fsumcl2lem  11339  fsumcl  11341  sumsnf  11350  fsummulc2  11389  binom  11425  isumshft  11431  isumsplit  11432  geolim2  11453  cvgratnnlemseq  11467  cvgratz  11473  ef0lem  11601  efcj  11614  ef4p  11635  efgt1p  11637  tanval3ap  11655  efi4p  11658  sinadd  11677  cosadd  11678  tanaddap  11680  addsin  11683  demoivreALT  11714  opoe  11832  pythagtriplem4  12200  pythagtriplem12  12207  gzaddcl  12307  addccncf  13226  dvaddxxbr  13305  dvaddxx  13307  dviaddf  13309  dveflem  13327  sinperlem  13369  ptolemy  13385  tangtx  13399  sinkpi  13408  binom4  13537  2sqlem2  13591