Theorem addcl 7899

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772   + caddc 7777

This theorem was proved from axioms:  ax-addcl 7870

This theorem is referenced by:  adddir  7911  0cn  7912  addcli  7924  addcld  7939  muladd11  8052  peano2cn  8054  muladd11r  8075  add4  8080  cnegexlem3  8096  cnegex  8097  0cnALT  8109  negeu  8110  pncan  8125  2addsub  8133  addsubeq4  8134  nppcan2  8150  ppncan  8161  muladd  8303  mulsub  8320  recexap  8571  muleqadd  8586  conjmulap  8646  halfaddsubcl  9111  halfaddsub  9112  serf  10430  ser3add  10461  ser3sub  10462  ser0  10470  binom2  10587  binom3  10593  bernneq  10596  shftlem  10780  shftval2  10790  shftval5  10793  2shfti  10795  crre  10821  crim  10822  cjadd  10848  addcj  10855  sqabsadd  11019  absreimsq  11031  absreim  11032  abstri  11068  addcn2  11273  climadd  11289  clim2ser  11300  clim2ser2  11301  isermulc2  11303  serf0  11315  sumrbdclem  11340  fsum3cvg  11341  summodclem3  11343  summodclem2a  11344  zsumdc  11347  fsum3  11350  fsum3cvg2  11357  fsum3ser  11360  fsumcl2lem  11361  fsumcl  11363  sumsnf  11372  fsummulc2  11411  binom  11447  isumshft  11453  isumsplit  11454  geolim2  11475  cvgratnnlemseq  11489  cvgratz  11495  ef0lem  11623  efcj  11636  ef4p  11657  efgt1p  11659  tanval3ap  11677  efi4p  11680  sinadd  11699  cosadd  11700  tanaddap  11702  addsin  11705  demoivreALT  11736  opoe  11854  pythagtriplem4  12222  pythagtriplem12  12229  gzaddcl  12329  addccncf  13380  dvaddxxbr  13459  dvaddxx  13461  dviaddf  13463  dveflem  13481  sinperlem  13523  ptolemy  13539  tangtx  13553  sinkpi  13562  binom4  13691  2sqlem2  13745