Theorem addcl 11192

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   + caddc 11113

This theorem was proved from axioms:  ax-addcl 11170

This theorem is referenced by:  adddir  11205  0cn  11206  addcli  11220  addcld  11233  muladd11  11384  peano2cn  11386  muladd11r  11427  add4  11434  0cnALT2  11449  negeu  11450  pncan  11466  2addsub  11474  addsubeq4  11475  nppcan2  11491  pnpcan  11499  ppncan  11502  muladd  11646  mulsub  11657  recex  11846  muleqadd  11858  conjmul  11931  halfaddsubcl  12444  halfaddsub  12445  serf  13996  seradd  14010  sersub  14011  binom3  14187  bernneq  14192  lswccatn0lsw  14541  revccat  14716  2cshwcshw  14776  shftlem  15015  shftval2  15022  shftval5  15025  2shfti  15027  crre  15061  crim  15062  cjadd  15088  addcj  15095  sqabsadd  15229  absreimsq  15239  absreim  15240  abstri  15277  sqreulem  15306  sqreu  15307  addcn2  15538  o1add  15558  climadd  15576  clim2ser  15601  clim2ser2  15602  isermulc2  15604  isercolllem3  15613  summolem3  15660  summolem2a  15661  fsumcl  15679  fsummulc2  15730  fsumrelem  15753  binom  15776  isumsplit  15786  risefacval2  15954  risefaccl  15959  risefallfac  15968  risefacp1  15973  binomfallfac  15985  binomrisefac  15986  bpoly3  16002  efcj  16035  ef4p  16056  tanval3  16077  efi4p  16080  sinadd  16107  cosadd  16108  tanadd  16110  addsin  16113  demoivreALT  16144  opoe  16306  pythagtriplem4  16752  pythagtriplem12  16759  pythagtriplem14  16761  pythagtriplem16  16763  gzaddcl  16870  cnaddablx  19736  cnaddabl  19737  cncrng  20966  cnperf  24336  cnlmod  24656  cnstrcvs  24657  cncvs  24661  dvaddbr  25455  dvaddf  25459  dveflem  25496  plyaddcl  25734  plymulcl  25735  plysubcl  25736  coeaddlem  25763  dgrcolem1  25787  dgrcolem2  25788  quotlem  25813  quotcl2  25815  quotdgr  25816  sinperlem  25990  ptolemy  26006  tangtx  26015  sinkpi  26031  efif1olem2  26052  logrnaddcl  26083  logneg  26096  logimul  26122  cxpadd  26187  binom4  26355  atanf  26385  atanneg  26412  atancj  26415  efiatan  26417  atanlogaddlem  26418  atanlogadd  26419  atanlogsublem  26420  atanlogsub  26421  efiatan2  26422  2efiatan  26423  tanatan  26424  cosatan  26426  cosatanne0  26427  atantan  26428  atanbndlem  26430  atans2  26436  dvatan  26440  atantayl  26442  efrlim  26474  dfef2  26475  gamcvg2lem  26563  ftalem7  26583  prmorcht  26682  bposlem9  26795  lgsquad2lem1  26887  2sqlem2  26921  cncph  30072  hhssnv  30517  hoadddir  31057  superpos  31607  knoppcnlem8  35376  cos2h  36479  tan2h  36480  ftc1anclem3  36563  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  facp2  40959  fac2xp3  41020  sumcubes  41211  fsumsermpt  44295  stirlinglem5  44794  stirlinglem7  44796  cnapbmcpd  46003  fmtnodvds  46212  opoeALTV  46351  mogoldbblem  46388