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

Theorem addcl 9376
Description: Alias for ax-addcl 9354, for naming consistency with addcli 9402. Use this theorem instead of ax-addcl 9354 or axaddcl 9330. (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 9354 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 1756  (class class class)co 6103   CCcc 9292    + caddc 9297
This theorem was proved from axioms:  ax-addcl 9354
This theorem is referenced by:  adddir  9389  0cn  9390  addcli  9402  addcld  9417  muladd11  9551  peano2cn  9553  add4  9597  0cnALT  9611  negeu  9612  pncan  9628  2addsub  9636  addsubeq4  9637  nppcan2  9652  ppncan  9663  muladd  9789  mulsub  9799  recex  9980  muleqadd  9992  conjmul  10060  halfaddsubcl  10569  halfaddsub  10570  uzindOLD  10748  serf  11846  seradd  11860  sersub  11861  binom3  11997  bernneq  12002  lswccatn0lsw  12299  revccat  12418  shftlem  12569  shftval2  12576  shftval5  12579  2shfti  12581  crre  12615  crim  12616  cjadd  12642  addcj  12649  sqabsadd  12783  absreimsq  12793  absreim  12794  abstri  12830  sqreulem  12859  sqreu  12860  addcn2  13083  o1add  13103  climadd  13121  clim2ser  13144  clim2ser2  13145  isermulc2  13147  isercolllem3  13156  summolem3  13203  summolem2a  13204  fsumcl  13222  fsummulc2  13263  fsumrelem  13282  binom  13305  isumsplit  13315  efcj  13389  ef4p  13409  tanval3  13430  efi4p  13433  sinadd  13460  cosadd  13461  tanadd  13463  addsin  13466  demoivreALT  13497  opoe  13890  pythagtriplem4  13898  pythagtriplem12  13905  pythagtriplem14  13907  pythagtriplem16  13909  gzaddcl  14010  cnaddablx  16360  cnaddabl  16361  cncrng  17849  cnperf  20409  dvaddbr  21424  dvaddf  21428  dveflem  21463  plyaddcl  21700  plymulcl  21701  plysubcl  21702  coeaddlem  21728  dgrcolem1  21752  dgrcolem2  21753  quotlem  21778  quotcl2  21780  quotdgr  21781  sinperlem  21954  ptolemy  21970  tangtx  21979  sinkpi  21993  efgh  22009  efif1olem2  22011  logrnaddcl  22038  logneg  22048  logimul  22075  cxpadd  22136  binom4  22257  atanf  22287  atanneg  22314  atancj  22317  efiatan  22319  atanlogaddlem  22320  atanlogadd  22321  atanlogsublem  22322  atanlogsub  22323  efiatan2  22324  2efiatan  22325  tanatan  22326  cosatan  22328  cosatanne0  22329  atantan  22330  atanbndlem  22332  atans2  22338  dvatan  22342  atantayl  22344  efrlim  22375  dfef2  22376  ftalem7  22428  prmorcht  22528  bposlem9  22643  lgsquad2lem1  22709  2sqlem2  22715  wlkdvspthlem  23518  gxadd  23774  cncph  24231  hhssnv  24677  hoadddir  25220  superpos  25770  gamcvg2lem  27057  risefacval2  27525  risefaccl  27530  risefallfac  27539  risefacp1  27544  binomfallfac  27556  binomrisefac  27557  bpoly3  28213  cos2h  28435  tan2h  28436  dvtanlem  28453  ftc1anclem3  28481  ftc1anclem7  28485  ftc1anclem8  28486  ftc1anc  28487  stirlinglem5  29885  stirlinglem7  29887  cnapbmcpd  30181  wwlkext2clwwlk  30477  cshwlemma1  30501
  Copyright terms: Public domain W3C validator