Theorem addcl 7997

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

Assertion

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

Proof of Theorem addcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   + caddc 7875

This theorem was proved from axioms:  ax-addcl 7968

This theorem is referenced by:  adddir  8010  0cn  8011  addcli  8023  addcld  8039  muladd11  8152  peano2cn  8154  muladd11r  8175  add4  8180  cnegexlem3  8196  cnegex  8197  0cnALT  8209  negeu  8210  pncan  8225  2addsub  8233  addsubeq4  8234  nppcan2  8250  ppncan  8261  muladd  8403  mulsub  8420  recexap  8672  muleqadd  8687  conjmulap  8748  ofnegsub  8981  halfaddsubcl  9215  halfaddsub  9216  serf  10554  ser3add  10593  ser3sub  10594  ser0  10604  binom2  10722  binom3  10728  bernneq  10731  shftlem  10960  shftval2  10970  shftval5  10973  2shfti  10975  crre  11001  crim  11002  cjadd  11028  addcj  11035  sqabsadd  11199  absreimsq  11211  absreim  11212  abstri  11248  addcn2  11453  climadd  11469  clim2ser  11480  clim2ser2  11481  isermulc2  11483  serf0  11495  sumrbdclem  11520  fsum3cvg  11521  summodclem3  11523  summodclem2a  11524  zsumdc  11527  fsum3  11530  fsum3cvg2  11537  fsum3ser  11540  fsumcl2lem  11541  fsumcl  11543  sumsnf  11552  fsummulc2  11591  binom  11627  isumshft  11633  isumsplit  11634  geolim2  11655  cvgratnnlemseq  11669  cvgratz  11675  ef0lem  11803  efcj  11816  ef4p  11837  efgt1p  11839  tanval3ap  11857  efi4p  11860  sinadd  11879  cosadd  11880  tanaddap  11882  addsin  11885  demoivreALT  11917  opoe  12036  pythagtriplem4  12406  pythagtriplem12  12413  gzaddcl  12515  cncrng  14057  addccncf  14754  dvaddxxbr  14850  dvaddxx  14852  dviaddf  14854  dveflem  14872  plyaddcl  14900  plymulcl  14901  plysubcl  14902  sinperlem  14943  ptolemy  14959  tangtx  14973  sinkpi  14982  binom4  15111  2sqlem2  15202