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

Theorem addcl 9360
Description: Alias for ax-addcl 9338, for naming consistency with addcli 9386. Use this theorem instead of ax-addcl 9338 or axaddcl 9314. (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 9338 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1761  (class class class)co 6090   CCcc 9276    + caddc 9281
This theorem was proved from axioms:  ax-addcl 9338
This theorem is referenced by:  adddir  9373  0cn  9374  addcli  9386  addcld  9401  muladd11  9535  peano2cn  9537  add4  9581  0cnALT  9595  negeu  9596  pncan  9612  2addsub  9620  addsubeq4  9621  nppcan2  9636  ppncan  9647  muladd  9773  mulsub  9783  recex  9964  muleqadd  9976  conjmul  10044  halfaddsubcl  10553  halfaddsub  10554  uzindOLD  10732  serf  11830  seradd  11844  sersub  11845  binom3  11981  bernneq  11986  lswccatn0lsw  12283  revccat  12402  shftlem  12553  shftval2  12560  shftval5  12563  2shfti  12565  crre  12599  crim  12600  cjadd  12626  addcj  12633  sqabsadd  12767  absreimsq  12777  absreim  12778  abstri  12814  sqreulem  12843  sqreu  12844  addcn2  13067  o1add  13087  climadd  13105  clim2ser  13128  clim2ser2  13129  isermulc2  13131  isercolllem3  13140  summolem3  13187  summolem2a  13188  fsumcl  13206  fsummulc2  13247  fsumrelem  13266  binom  13289  isumsplit  13299  efcj  13373  ef4p  13393  tanval3  13414  efi4p  13417  sinadd  13444  cosadd  13445  tanadd  13447  addsin  13450  demoivreALT  13481  opoe  13874  pythagtriplem4  13882  pythagtriplem12  13889  pythagtriplem14  13891  pythagtriplem16  13893  gzaddcl  13994  cnaddablx  16341  cnaddabl  16342  cncrng  17796  cnperf  20356  dvaddbr  21371  dvaddf  21375  dveflem  21410  plyaddcl  21647  plymulcl  21648  plysubcl  21649  coeaddlem  21675  dgrcolem1  21699  dgrcolem2  21700  quotlem  21725  quotcl2  21727  quotdgr  21728  sinperlem  21901  ptolemy  21917  tangtx  21926  sinkpi  21940  efgh  21956  efif1olem2  21958  logrnaddcl  21985  logneg  21995  logimul  22022  cxpadd  22083  binom4  22204  atanf  22234  atanneg  22261  atancj  22264  efiatan  22266  atanlogaddlem  22267  atanlogadd  22268  atanlogsublem  22269  atanlogsub  22270  efiatan2  22271  2efiatan  22272  tanatan  22273  cosatan  22275  cosatanne0  22276  atantan  22277  atanbndlem  22279  atans2  22285  dvatan  22289  atantayl  22291  efrlim  22322  dfef2  22323  ftalem7  22375  prmorcht  22475  bposlem9  22590  lgsquad2lem1  22656  2sqlem2  22662  wlkdvspthlem  23441  gxadd  23697  cncph  24154  hhssnv  24600  hoadddir  25143  superpos  25693  gamcvg2lem  26975  risefacval2  27442  risefaccl  27447  risefallfac  27456  risefacp1  27461  binomfallfac  27473  binomrisefac  27474  bpoly3  28130  cos2h  28348  tan2h  28349  dvtanlem  28366  ftc1anclem3  28394  ftc1anclem7  28398  ftc1anclem8  28399  ftc1anc  28400  stirlinglem5  29798  stirlinglem7  29800  cnapbmcpd  30094  wwlkext2clwwlk  30390  cshwlemma1  30414
  Copyright terms: Public domain W3C validator