Theorem addcl 7465

Description: Alias for ax-addcl 7439, for naming consistency with addcli 7490. Use this theorem instead of ax-addcl 7439 or axaddcl 7399. (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 7439	1 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1438  (class class class)co 5652   CCcc 7346   + caddc 7351

This theorem was proved from axioms:  ax-addcl 7439

This theorem is referenced by:  adddir  7477  0cn  7478  addcli  7490  addcld  7505  muladd11  7613  peano2cn  7615  muladd11r  7636  add4  7641  cnegexlem3  7657  cnegex  7658  0cnALT  7670  negeu  7671  pncan  7686  2addsub  7694  addsubeq4  7695  nppcan2  7711  ppncan  7722  muladd  7860  mulsub  7877  recexap  8120  muleqadd  8135  conjmulap  8194  halfaddsubcl  8647  halfaddsub  8648  serf  9896  iseqseq3  9898  iserf  9899  iseradd  9930  isersub  9932  iser0  9943  ser0  9945  binom2  10061  binom3  10067  bernneq  10070  shftlem  10246  shftval2  10256  shftval5  10259  2shfti  10261  crre  10287  crim  10288  cjadd  10314  addcj  10321  sqabsadd  10484  absreimsq  10496  absreim  10497  abstri  10533  addcn2  10695  climadd  10710  clim2ser  10721  clim2ser2  10722  iisermulc2  10724  serf0  10737  isumrblem  10761  fisumcvg  10762  fsum3cvg  10763  isummolem3  10766  isummolem2a  10767  zisum  10770  fisum  10774  fisumcvg2  10782  fsum3cvg2  10783  fisumser  10786  fsumcl2lem  10788  fsumcl  10790  sumsnf  10799  fsummulc2  10838  binom  10874  isumshft  10880  isumsplit  10881  geolim2  10902  cvgratnnlemseq  10916  cvgratz  10922  ef0lem  10946  efcj  10959  ef4p  10980  efgt1p  10982  tanval3ap  11001  efi4p  11004  sinadd  11023  cosadd  11024  tanaddap  11026  addsin  11029  demoivreALT  11059  opoe  11169