Theorem addcl 11285

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

Assertion

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

Proof of Theorem addcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   + caddc 11206

This proof depends on axioms:  ax-addcl 11263

This theorem is used by:  mpoaddf  11297  adddir  11300  0cn  11301  addcli  11318  addcld  11331  muladd11  11483  peano2cn  11485  muladd11r  11526  add4  11534  0cnALT2  11549  negeu  11550  pncan  11566  2addsub  11574  addsubeq4  11575  nppcan2  11592  pnpcan  11600  ppncan  11603  muladd  11751  mulsub  11762  recex  11951  muleqadd  11963  conjmul  12037  halfaddsubcl  12581  halfaddsub  12582  serf  14176  seradd  14190  sersub  14191  binom3  14371  bernneq  14376  lswccatn0lsw  14741  revccat  14919  2cshwcshw  14980  shftlem  15226  shftval2  15233  shftval5  15236  2shfti  15238  crre  15286  crim  15287  cjadd  15313  addcj  15320  sqabsadd  15454  absreimsq  15464  absreim  15465  abstri  15503  sqreulem  15532  sqreu  15533  addcn2  15766  o1add  15786  climadd  15804  clim2ser  15827  clim2ser2  15828  isermulc2  15830  isercolllem3  15839  summolem3  15885  summolem2a  15886  fsumcl  15904  fsummulc2  15955  fsumrelem  15979  binom  16004  isumsplit  16014  risefacval2  16182  risefaccl  16187  risefallfac  16196  risefacp1  16200  binomfallfac  16212  binomrisefac  16213  bpoly3  16229  efcj  16263  ef4p  16286  tanval3  16307  efi4p  16310  sinadd  16337  cosadd  16338  tanadd  16340  addsin  16343  demoivreALT  16374  opoe  16538  pythagtriplem4  17002  pythagtriplem12  17009  pythagtriplem14  17011  pythagtriplem16  17013  gzaddcl  17120  cnaddablx  20087  cnaddabl  20088  cncrng  21704  cnperf  25145  cnlmod  25466  cnstrcvs  25467  cncvs  25471  dvaddbr  26263  dvaddf  26267  dveflem  26304  plyaddcl  26544  plymulcl  26545  plysubcl  26546  coeaddlem  26573  dgrcolem1  26597  dgrcolem2  26598  quotlem  26626  quotcl2  26628  quotdgr  26629  sinperlem  26814  ptolemy  26830  tangtx  26839  sinkpi  26855  efif1olem2  26876  logrnaddcl  26907  logneg  26921  logimul  26947  cxpadd  27012  binom4  27183  atanf  27213  atanneg  27240  atancj  27243  efiatan  27245  atanlogaddlem  27246  atanlogadd  27247  atanlogsublem  27248  atanlogsub  27249  efiatan2  27250  2efiatan  27251  tanatan  27252  cosatan  27254  cosatanne0  27255  atantan  27256  atanbndlem  27258  atans2  27264  dvatan  27268  atantayl  27270  efrlim  27302  dfef2  27303  gamcvg2lem  27391  ftalem7  27411  prmorcht  27510  bposlem9  27624  lgsquad2lem1  27716  2sqlem2  27750  cncph  31426  hhssnv  31871  hoadddir  32411  superpos  32961  knoppcnlem8  37458  cos2h  38627  tan2h  38628  ftc1anclem3  38706  ftc1anclem7  38710  ftc1anclem8  38711  ftc1anc  38712  facp2  43286  sumcubes  43463  fsumsermpt  46684  stirlinglem5  47181  stirlinglem7  47183  cnapbmcpd  48458  fmtnodvds  48722  opoeALTV  48874  mogoldbblem  48911