MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcl Unicode version

Theorem addcl 8819
Description: Alias for ax-addcl 8797, for naming consistency with addcli 8841. Use this theorem instead of ax-addcl 8797 or axaddcl 8773. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addcl  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 8797 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740
This theorem is referenced by:  adddir  8830  0cn  8831  addcli  8841  addcld  8854  muladd11  8982  peano2cn  8984  add4  9027  0cnALT  9041  negeu  9042  pncan  9057  2addsub  9065  addsubeq4  9066  nppcan2  9078  ppncan  9089  muladd  9212  mulsub  9222  recex  9400  muleqadd  9412  conjmul  9477  halfaddsubcl  9944  halfaddsub  9945  uzindOLD  10106  serf  11074  seradd  11088  sersub  11089  binom3  11222  bernneq  11227  revccat  11484  shftlem  11563  shftval2  11570  shftval5  11573  2shfti  11575  crre  11599  crim  11600  cjadd  11626  addcj  11633  sqabsadd  11767  absreimsq  11777  absreim  11778  abstri  11814  sqreulem  11843  sqreu  11844  addcn2  12067  o1add  12087  climadd  12105  clim2ser  12128  clim2ser2  12129  isermulc2  12131  isercolllem3  12140  summolem3  12187  summolem2a  12188  fsumcl  12206  fsummulc2  12246  fsumrelem  12265  binom  12288  isumsplit  12299  efcj  12373  ef4p  12393  tanval3  12414  efi4p  12417  sinadd  12444  cosadd  12445  tanadd  12447  addsin  12450  demoivreALT  12481  opoe  12864  pythagtriplem4  12872  pythagtriplem12  12879  pythagtriplem14  12881  pythagtriplem16  12883  gzaddcl  12984  cnaddablx  15158  cnaddabl  15159  cncrng  16395  cnperf  18325  dvaddbr  19287  dvaddf  19291  dveflem  19326  plyaddcl  19602  plymulcl  19603  plysubcl  19604  coeaddlem  19630  dgrcolem1  19654  dgrcolem2  19655  quotlem  19680  quotcl2  19682  quotdgr  19683  sinperlem  19848  ptolemy  19864  tangtx  19873  sinkpi  19887  efgh  19903  efif1olem2  19905  logrnaddcl  19931  logneg  19941  logimul  19968  cxpadd  20026  binom4  20146  atanf  20176  atanneg  20203  atancj  20206  efiatan  20208  atanlogaddlem  20209  atanlogadd  20210  atanlogsublem  20211  atanlogsub  20212  efiatan2  20213  2efiatan  20214  tanatan  20215  cosatan  20217  cosatanne0  20218  atantan  20219  atanbndlem  20221  atans2  20227  dvatan  20231  atantayl  20233  efrlim  20264  dfef2  20265  ftalem7  20316  prmorcht  20416  bposlem9  20531  lgsquad2lem1  20597  2sqlem2  20603  gxadd  20942  cncph  21397  hhssnv  21841  hoadddir  22384  superpos  22934  dmgmseqn0  23696  bpoly3  24793  fsumcube  24795  2wsms  25608  lvsovso  25626  sigadd  25649  distsava  25689  stoweidlem1  27750  stoweidlem11  27760  stoweidlem13  27762  stirlinglem5  27827  stirlinglem7  27829
This theorem was proved from axioms:  ax-addcl 8797
  Copyright terms: Public domain W3C validator