Theorem addcl 7936

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  (class class class)co 5875  ℂcc 7809   + caddc 7814

This theorem was proved from axioms:  ax-addcl 7907

This theorem is referenced by:  adddir  7948  0cn  7949  addcli  7961  addcld  7977  muladd11  8090  peano2cn  8092  muladd11r  8113  add4  8118  cnegexlem3  8134  cnegex  8135  0cnALT  8147  negeu  8148  pncan  8163  2addsub  8171  addsubeq4  8172  nppcan2  8188  ppncan  8199  muladd  8341  mulsub  8358  recexap  8610  muleqadd  8625  conjmulap  8686  halfaddsubcl  9152  halfaddsub  9153  serf  10474  ser3add  10505  ser3sub  10506  ser0  10514  binom2  10632  binom3  10638  bernneq  10641  shftlem  10825  shftval2  10835  shftval5  10838  2shfti  10840  crre  10866  crim  10867  cjadd  10893  addcj  10900  sqabsadd  11064  absreimsq  11076  absreim  11077  abstri  11113  addcn2  11318  climadd  11334  clim2ser  11345  clim2ser2  11346  isermulc2  11348  serf0  11360  sumrbdclem  11385  fsum3cvg  11386  summodclem3  11388  summodclem2a  11389  zsumdc  11392  fsum3  11395  fsum3cvg2  11402  fsum3ser  11405  fsumcl2lem  11406  fsumcl  11408  sumsnf  11417  fsummulc2  11456  binom  11492  isumshft  11498  isumsplit  11499  geolim2  11520  cvgratnnlemseq  11534  cvgratz  11540  ef0lem  11668  efcj  11681  ef4p  11702  efgt1p  11704  tanval3ap  11722  efi4p  11725  sinadd  11744  cosadd  11745  tanaddap  11747  addsin  11750  demoivreALT  11781  opoe  11900  pythagtriplem4  12268  pythagtriplem12  12275  gzaddcl  12375  cncrng  13466  addccncf  14089  dvaddxxbr  14168  dvaddxx  14170  dviaddf  14172  dveflem  14190  sinperlem  14232  ptolemy  14248  tangtx  14262  sinkpi  14271  binom4  14400  2sqlem2  14465