Theorem addcl 8120

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

Assertion

Ref	Expression
addcl	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

Proof of Theorem addcl

Step	Hyp	Ref	Expression
1		ax-addcl 8091	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200  (class class class)co 6000   CCcc 7993   + caddc 7998

This theorem was proved from axioms:  ax-addcl 8091

This theorem is referenced by:  adddir  8133  0cn  8134  addcli  8146  addcld  8162  muladd11  8275  peano2cn  8277  muladd11r  8298  add4  8303  cnegexlem3  8319  cnegex  8320  0cnALT  8332  negeu  8333  pncan  8348  2addsub  8356  addsubeq4  8357  nppcan2  8373  ppncan  8384  muladd  8526  mulsub  8543  recexap  8796  muleqadd  8811  conjmulap  8872  ofnegsub  9105  halfaddsubcl  9340  halfaddsub  9341  serf  10700  ser3add  10739  ser3sub  10740  ser0  10750  binom2  10868  binom3  10874  bernneq  10877  lswccatn0lsw  11141  shftlem  11322  shftval2  11332  shftval5  11335  2shfti  11337  crre  11363  crim  11364  cjadd  11390  addcj  11397  sqabsadd  11561  absreimsq  11573  absreim  11574  abstri  11610  addcn2  11816  climadd  11832  clim2ser  11843  clim2ser2  11844  isermulc2  11846  serf0  11858  sumrbdclem  11883  fsum3cvg  11884  summodclem3  11886  summodclem2a  11887  zsumdc  11890  fsum3  11893  fsum3cvg2  11900  fsum3ser  11903  fsumcl2lem  11904  fsumcl  11906  sumsnf  11915  fsummulc2  11954  binom  11990  isumshft  11996  isumsplit  11997  geolim2  12018  cvgratnnlemseq  12032  cvgratz  12038  ef0lem  12166  efcj  12179  ef4p  12200  efgt1p  12202  tanval3ap  12220  efi4p  12223  sinadd  12242  cosadd  12243  tanaddap  12245  addsin  12248  demoivreALT  12280  opoe  12401  pythagtriplem4  12786  pythagtriplem12  12793  gzaddcl  12895  cncrng  14527  addccncf  15268  dvaddxxbr  15369  dvaddxx  15371  dviaddf  15373  dveflem  15394  plyaddcl  15422  plymulcl  15423  plysubcl  15424  sinperlem  15476  ptolemy  15492  tangtx  15506  sinkpi  15515  binom4  15647  lgsquad2lem1  15754  2sqlem2  15788