Theorem addcl 11200

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

Assertion

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

Proof of Theorem addcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   + caddc 11121

This proof depends on axioms:  ax-addcl 11178

This theorem is used by:  mpoaddf  11212  adddir  11215  0cn  11216  addcli  11233  addcld  11246  muladd11  11398  peano2cn  11400  muladd11r  11441  add4  11449  0cnALT2  11464  negeu  11465  pncan  11481  2addsub  11489  addsubeq4  11490  nppcan2  11507  pnpcan  11515  ppncan  11518  muladd  11664  mulsub  11675  recex  11864  muleqadd  11876  conjmul  11950  halfaddsubcl  12494  halfaddsub  12495  serf  14086  seradd  14100  sersub  14101  binom3  14280  bernneq  14285  lswccatn0lsw  14650  revccat  14827  2cshwcshw  14888  shftlem  15131  shftval2  15138  shftval5  15141  2shfti  15143  crre  15191  crim  15192  cjadd  15218  addcj  15225  sqabsadd  15359  absreimsq  15369  absreim  15370  abstri  15408  sqreulem  15437  sqreu  15438  addcn2  15671  o1add  15691  climadd  15709  clim2ser  15732  clim2ser2  15733  isermulc2  15735  isercolllem3  15744  summolem3  15791  summolem2a  15792  fsumcl  15810  fsummulc2  15861  fsumrelem  15885  binom  15910  isumsplit  15920  risefacval2  16090  risefaccl  16095  risefallfac  16104  risefacp1  16108  binomfallfac  16120  binomrisefac  16121  bpoly3  16137  efcj  16171  ef4p  16194  tanval3  16215  efi4p  16218  sinadd  16245  cosadd  16246  tanadd  16248  addsin  16251  demoivreALT  16282  opoe  16446  pythagtriplem4  16904  pythagtriplem12  16911  pythagtriplem14  16913  pythagtriplem16  16915  gzaddcl  17022  cnaddablx  19969  cnaddabl  19970  cncrng  21580  cnperf  25015  cnlmod  25336  cnstrcvs  25337  cncvs  25341  dvaddbr  26134  dvaddf  26138  dveflem  26175  plyaddcl  26414  plymulcl  26415  plysubcl  26416  coeaddlem  26443  dgrcolem1  26467  dgrcolem2  26468  quotlem  26498  quotcl2  26500  quotdgr  26501  sinperlem  26682  ptolemy  26698  tangtx  26707  sinkpi  26724  efif1olem2  26745  logrnaddcl  26776  logneg  26790  logimul  26816  cxpadd  26881  binom4  27052  atanf  27082  atanneg  27109  atancj  27112  efiatan  27114  atanlogaddlem  27115  atanlogadd  27116  atanlogsublem  27117  atanlogsub  27118  efiatan2  27119  2efiatan  27120  tanatan  27121  cosatan  27123  cosatanne0  27124  atantan  27125  atanbndlem  27127  atans2  27133  dvatan  27137  atantayl  27139  efrlim  27171  dfef2  27172  gamcvg2lem  27260  ftalem7  27280  prmorcht  27379  bposlem9  27493  lgsquad2lem1  27585  2sqlem2  27619  cncph  31208  hhssnv  31653  hoadddir  32193  superpos  32743  knoppcnlem8  37129  cos2h  38302  tan2h  38303  ftc1anclem3  38386  ftc1anclem7  38390  ftc1anclem8  38391  ftc1anc  38392  facp2  42950  sumcubes  43114  fsumsermpt  46335  stirlinglem5  46832  stirlinglem7  46834  cnapbmcpd  48072  fmtnodvds  48336  opoeALTV  48488  mogoldbblem  48525