Theorem addcl 11210

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

Assertion

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

Proof of Theorem addcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126   + caddc 11131

This proof depends on axioms:  ax-addcl 11188

This theorem is used by:  mpoaddf  11222  adddir  11225  0cn  11226  addcli  11243  addcld  11256  muladd11  11408  peano2cn  11410  muladd11r  11451  add4  11459  0cnALT2  11474  negeu  11475  pncan  11491  2addsub  11499  addsubeq4  11500  nppcan2  11517  pnpcan  11525  ppncan  11528  muladd  11674  mulsub  11685  recex  11874  muleqadd  11886  conjmul  11960  halfaddsubcl  12504  halfaddsub  12505  serf  14098  seradd  14112  sersub  14113  binom3  14292  bernneq  14297  lswccatn0lsw  14662  revccat  14839  2cshwcshw  14900  shftlem  15145  shftval2  15152  shftval5  15155  2shfti  15157  crre  15205  crim  15206  cjadd  15232  addcj  15239  sqabsadd  15373  absreimsq  15383  absreim  15384  abstri  15422  sqreulem  15451  sqreu  15452  addcn2  15685  o1add  15705  climadd  15723  clim2ser  15746  clim2ser2  15747  isermulc2  15749  isercolllem3  15758  summolem3  15804  summolem2a  15805  fsumcl  15823  fsummulc2  15874  fsumrelem  15898  binom  15923  isumsplit  15933  risefacval2  16103  risefaccl  16108  risefallfac  16117  risefacp1  16121  binomfallfac  16133  binomrisefac  16134  bpoly3  16150  efcj  16184  ef4p  16207  tanval3  16228  efi4p  16231  sinadd  16258  cosadd  16259  tanadd  16261  addsin  16264  demoivreALT  16295  opoe  16459  pythagtriplem4  16917  pythagtriplem12  16924  pythagtriplem14  16926  pythagtriplem16  16928  gzaddcl  17035  cnaddablx  20001  cnaddabl  20002  cncrng  21612  cnperf  25053  cnlmod  25374  cnstrcvs  25375  cncvs  25379  dvaddbr  26172  dvaddf  26176  dveflem  26213  plyaddcl  26453  plymulcl  26454  plysubcl  26455  coeaddlem  26482  dgrcolem1  26506  dgrcolem2  26507  quotlem  26537  quotcl2  26539  quotdgr  26540  sinperlem  26725  ptolemy  26741  tangtx  26750  sinkpi  26767  efif1olem2  26788  logrnaddcl  26819  logneg  26833  logimul  26859  cxpadd  26924  binom4  27095  atanf  27125  atanneg  27152  atancj  27155  efiatan  27157  atanlogaddlem  27158  atanlogadd  27159  atanlogsublem  27160  atanlogsub  27161  efiatan2  27162  2efiatan  27163  tanatan  27164  cosatan  27166  cosatanne0  27167  atantan  27168  atanbndlem  27170  atans2  27176  dvatan  27180  atantayl  27182  efrlim  27214  dfef2  27215  gamcvg2lem  27303  ftalem7  27323  prmorcht  27422  bposlem9  27536  lgsquad2lem1  27628  2sqlem2  27662  cncph  31308  hhssnv  31753  hoadddir  32293  superpos  32843  knoppcnlem8  37205  cos2h  38373  tan2h  38374  ftc1anclem3  38452  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  facp2  43017  sumcubes  43196  fsumsermpt  46417  stirlinglem5  46914  stirlinglem7  46916  cnapbmcpd  48191  fmtnodvds  48455  opoeALTV  48607  mogoldbblem  48644