Theorem addcl 11142

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  (class class class)co 7362  ℂcc 11058   + caddc 11063

This theorem was proved from axioms:  ax-addcl 11120

This theorem is referenced by:  adddir  11155  0cn  11156  addcli  11170  addcld  11183  muladd11  11334  peano2cn  11336  muladd11r  11377  add4  11384  0cnALT2  11399  negeu  11400  pncan  11416  2addsub  11424  addsubeq4  11425  nppcan2  11441  pnpcan  11449  ppncan  11452  muladd  11596  mulsub  11607  recex  11796  muleqadd  11808  conjmul  11881  halfaddsubcl  12394  halfaddsub  12395  serf  13946  seradd  13960  sersub  13961  binom3  14137  bernneq  14142  lswccatn0lsw  14491  revccat  14666  2cshwcshw  14726  shftlem  14965  shftval2  14972  shftval5  14975  2shfti  14977  crre  15011  crim  15012  cjadd  15038  addcj  15045  sqabsadd  15179  absreimsq  15189  absreim  15190  abstri  15227  sqreulem  15256  sqreu  15257  addcn2  15488  o1add  15508  climadd  15526  clim2ser  15551  clim2ser2  15552  isermulc2  15554  isercolllem3  15563  summolem3  15610  summolem2a  15611  fsumcl  15629  fsummulc2  15680  fsumrelem  15703  binom  15726  isumsplit  15736  risefacval2  15904  risefaccl  15909  risefallfac  15918  risefacp1  15923  binomfallfac  15935  binomrisefac  15936  bpoly3  15952  efcj  15985  ef4p  16006  tanval3  16027  efi4p  16030  sinadd  16057  cosadd  16058  tanadd  16060  addsin  16063  demoivreALT  16094  opoe  16256  pythagtriplem4  16702  pythagtriplem12  16709  pythagtriplem14  16711  pythagtriplem16  16713  gzaddcl  16820  cnaddablx  19660  cnaddabl  19661  cncrng  20855  cnperf  24220  cnlmod  24540  cnstrcvs  24541  cncvs  24545  dvaddbr  25339  dvaddf  25343  dveflem  25380  plyaddcl  25618  plymulcl  25619  plysubcl  25620  coeaddlem  25647  dgrcolem1  25671  dgrcolem2  25672  quotlem  25697  quotcl2  25699  quotdgr  25700  sinperlem  25874  ptolemy  25890  tangtx  25899  sinkpi  25915  efif1olem2  25936  logrnaddcl  25967  logneg  25980  logimul  26006  cxpadd  26071  binom4  26237  atanf  26267  atanneg  26294  atancj  26297  efiatan  26299  atanlogaddlem  26300  atanlogadd  26301  atanlogsublem  26302  atanlogsub  26303  efiatan2  26304  2efiatan  26305  tanatan  26306  cosatan  26308  cosatanne0  26309  atantan  26310  atanbndlem  26312  atans2  26318  dvatan  26322  atantayl  26324  efrlim  26356  dfef2  26357  gamcvg2lem  26445  ftalem7  26465  prmorcht  26564  bposlem9  26677  lgsquad2lem1  26769  2sqlem2  26803  cncph  29824  hhssnv  30269  hoadddir  30809  superpos  31359  knoppcnlem8  35039  cos2h  36142  tan2h  36143  ftc1anclem3  36226  ftc1anclem7  36230  ftc1anclem8  36231  ftc1anc  36232  facp2  40624  fac2xp3  40685  fsumsermpt  43940  stirlinglem5  44439  stirlinglem7  44441  cnapbmcpd  45647  fmtnodvds  45856  opoeALTV  45995  mogoldbblem  46032