Theorem addcl 10056

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2030  (class class class)co 6690  ℂcc 9972   + caddc 9977

This theorem was proved from axioms:  ax-addcl 10034

This theorem is referenced by:  adddir  10069  0cn  10070  addcli  10082  addcld  10097  muladd11  10244  peano2cn  10246  muladd11r  10287  add4  10294  0cnALT  10308  negeu  10309  pncan  10325  2addsub  10333  addsubeq4  10334  nppcan2  10350  ppncan  10361  muladd  10500  mulsub  10511  recex  10697  muleqadd  10709  conjmul  10780  halfaddsubcl  11302  halfaddsub  11303  serf  12869  seradd  12883  sersub  12884  binom3  13025  bernneq  13030  lswccatn0lsw  13409  revccat  13561  2cshwcshw  13617  shftlem  13852  shftval2  13859  shftval5  13862  2shfti  13864  crre  13898  crim  13899  cjadd  13925  addcj  13932  sqabsadd  14066  absreimsq  14076  absreim  14077  abstri  14114  sqreulem  14143  sqreu  14144  addcn2  14368  o1add  14388  climadd  14406  clim2ser  14429  clim2ser2  14430  isermulc2  14432  isercolllem3  14441  summolem3  14489  summolem2a  14490  fsumcl  14508  fsummulc2  14560  fsumrelem  14583  binom  14606  isumsplit  14616  risefacval2  14785  risefaccl  14790  risefallfac  14799  risefacp1  14804  binomfallfac  14816  binomrisefac  14817  bpoly3  14833  efcj  14866  ef4p  14887  tanval3  14908  efi4p  14911  sinadd  14938  cosadd  14939  tanadd  14941  addsin  14944  demoivreALT  14975  opoe  15134  pythagtriplem4  15571  pythagtriplem12  15578  pythagtriplem14  15580  pythagtriplem16  15582  gzaddcl  15688  cnaddablx  18317  cnaddabl  18318  cncrng  19815  cnperf  22670  cnlmod  22986  cnstrcvs  22987  cncvs  22991  dvaddbr  23746  dvaddf  23750  dveflem  23787  plyaddcl  24021  plymulcl  24022  plysubcl  24023  coeaddlem  24050  dgrcolem1  24074  dgrcolem2  24075  quotlem  24100  quotcl2  24102  quotdgr  24103  sinperlem  24277  ptolemy  24293  tangtx  24302  sinkpi  24316  efif1olem2  24334  logrnaddcl  24366  logneg  24379  logimul  24405  cxpadd  24470  binom4  24622  atanf  24652  atanneg  24679  atancj  24682  efiatan  24684  atanlogaddlem  24685  atanlogadd  24686  atanlogsublem  24687  atanlogsub  24688  efiatan2  24689  2efiatan  24690  tanatan  24691  cosatan  24693  cosatanne0  24694  atantan  24695  atanbndlem  24697  atans2  24703  dvatan  24707  atantayl  24709  efrlim  24741  dfef2  24742  gamcvg2lem  24830  ftalem7  24850  prmorcht  24949  bposlem9  25062  lgsquad2lem1  25154  2sqlem2  25188  wwlksext2clwwlkOLD  27022  cncph  27802  hhssnv  28249  hoadddir  28791  superpos  29341  knoppcnlem8  32615  cos2h  33530  tan2h  33531  ftc1anclem3  33617  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  fsumsermpt  40129  stirlinglem5  40613  stirlinglem7  40615  cnapbmcpd  41635  fmtnodvds  41781  opoeALTV  41919  mogoldbblem  41954