Theorem addcl 10697

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2114  (class class class)co 7170  ℂcc 10613   + caddc 10618

This theorem was proved from axioms:  ax-addcl 10675

This theorem is referenced by:  adddir  10710  0cn  10711  addcli  10725  addcld  10738  muladd11  10888  peano2cn  10890  muladd11r  10931  add4  10938  0cnALT2  10953  negeu  10954  pncan  10970  2addsub  10978  addsubeq4  10979  nppcan2  10995  pnpcan  11003  ppncan  11006  muladd  11150  mulsub  11161  recex  11350  muleqadd  11362  conjmul  11435  halfaddsubcl  11948  halfaddsub  11949  serf  13490  seradd  13504  sersub  13505  binom3  13677  bernneq  13682  lswccatn0lsw  14034  revccat  14217  2cshwcshw  14276  shftlem  14517  shftval2  14524  shftval5  14527  2shfti  14529  crre  14563  crim  14564  cjadd  14590  addcj  14597  sqabsadd  14732  absreimsq  14742  absreim  14743  abstri  14780  sqreulem  14809  sqreu  14810  addcn2  15041  o1add  15061  climadd  15079  clim2ser  15104  clim2ser2  15105  isermulc2  15107  isercolllem3  15116  summolem3  15164  summolem2a  15165  fsumcl  15183  fsummulc2  15232  fsumrelem  15255  binom  15278  isumsplit  15288  risefacval2  15456  risefaccl  15461  risefallfac  15470  risefacp1  15475  binomfallfac  15487  binomrisefac  15488  bpoly3  15504  efcj  15537  ef4p  15558  tanval3  15579  efi4p  15582  sinadd  15609  cosadd  15610  tanadd  15612  addsin  15615  demoivreALT  15646  opoe  15808  pythagtriplem4  16256  pythagtriplem12  16263  pythagtriplem14  16265  pythagtriplem16  16267  gzaddcl  16373  cnaddablx  19107  cnaddabl  19108  cncrng  20238  cnperf  23572  cnlmod  23892  cnstrcvs  23893  cncvs  23897  dvaddbr  24690  dvaddf  24694  dveflem  24731  plyaddcl  24969  plymulcl  24970  plysubcl  24971  coeaddlem  24998  dgrcolem1  25022  dgrcolem2  25023  quotlem  25048  quotcl2  25050  quotdgr  25051  sinperlem  25225  ptolemy  25241  tangtx  25250  sinkpi  25266  efif1olem2  25287  logrnaddcl  25318  logneg  25331  logimul  25357  cxpadd  25422  binom4  25588  atanf  25618  atanneg  25645  atancj  25648  efiatan  25650  atanlogaddlem  25651  atanlogadd  25652  atanlogsublem  25653  atanlogsub  25654  efiatan2  25655  2efiatan  25656  tanatan  25657  cosatan  25659  cosatanne0  25660  atantan  25661  atanbndlem  25663  atans2  25669  dvatan  25673  atantayl  25675  efrlim  25707  dfef2  25708  gamcvg2lem  25796  ftalem7  25816  prmorcht  25915  bposlem9  26028  lgsquad2lem1  26120  2sqlem2  26154  cncph  28754  hhssnv  29199  hoadddir  29739  superpos  30289  knoppcnlem8  34318  cos2h  35391  tan2h  35392  ftc1anclem3  35475  ftc1anclem7  35479  ftc1anclem8  35480  ftc1anc  35481  facp2  39705  fac2xp3  39751  fsumsermpt  42662  stirlinglem5  43161  stirlinglem7  43163  cnapbmcpd  44321  fmtnodvds  44530  opoeALTV  44669  mogoldbblem  44706