Theorem addcl 7617

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1448  (class class class)co 5706  ℂcc 7498   + caddc 7503

This theorem was proved from axioms:  ax-addcl 7591

This theorem is referenced by:  adddir  7629  0cn  7630  addcli  7642  addcld  7657  muladd11  7766  peano2cn  7768  muladd11r  7789  add4  7794  cnegexlem3  7810  cnegex  7811  0cnALT  7823  negeu  7824  pncan  7839  2addsub  7847  addsubeq4  7848  nppcan2  7864  ppncan  7875  muladd  8013  mulsub  8030  recexap  8275  muleqadd  8290  conjmulap  8350  halfaddsubcl  8805  halfaddsub  8806  serf  10088  ser3add  10119  ser3sub  10120  ser0  10128  binom2  10244  binom3  10250  bernneq  10253  shftlem  10429  shftval2  10439  shftval5  10442  2shfti  10444  crre  10470  crim  10471  cjadd  10497  addcj  10504  sqabsadd  10667  absreimsq  10679  absreim  10680  abstri  10716  addcn2  10918  climadd  10934  clim2ser  10945  clim2ser2  10946  isermulc2  10948  serf0  10960  sumrbdclem  10984  fsum3cvg  10985  summodclem3  10988  summodclem2a  10989  zsumdc  10992  fsum3  10995  fsum3cvg2  11002  fsum3ser  11005  fsumcl2lem  11006  fsumcl  11008  sumsnf  11017  fsummulc2  11056  binom  11092  isumshft  11098  isumsplit  11099  geolim2  11120  cvgratnnlemseq  11134  cvgratz  11140  ef0lem  11164  efcj  11177  ef4p  11198  efgt1p  11200  tanval3ap  11219  efi4p  11222  sinadd  11241  cosadd  11242  tanaddap  11244  addsin  11247  demoivreALT  11277  opoe  11387  addccncf  12498