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

Theorem addcl 9563
Description: Alias for ax-addcl 9541, for naming consistency with addcli 9589. Use this theorem instead of ax-addcl 9541 or axaddcl 9517. (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 9541 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823  (class class class)co 6270   CCcc 9479    + caddc 9484
This theorem was proved from axioms:  ax-addcl 9541
This theorem is referenced by:  adddir  9576  0cn  9577  addcli  9589  addcld  9604  muladd11  9739  peano2cn  9741  add4  9785  0cnALT  9800  negeu  9801  pncan  9817  2addsub  9825  addsubeq4  9826  nppcan2  9841  ppncan  9852  muladd  9985  mulsub  9995  recex  10177  muleqadd  10189  conjmul  10257  halfaddsubcl  10767  halfaddsub  10768  uzindOLD  10953  serf  12117  seradd  12131  sersub  12132  binom3  12269  bernneq  12274  lswccatn0lsw  12596  revccat  12731  2cshwcshw  12784  shftlem  12983  shftval2  12990  shftval5  12993  2shfti  12995  crre  13029  crim  13030  cjadd  13056  addcj  13063  sqabsadd  13197  absreimsq  13207  absreim  13208  abstri  13245  sqreulem  13274  sqreu  13275  addcn2  13498  o1add  13518  climadd  13536  clim2ser  13559  clim2ser2  13560  isermulc2  13562  isercolllem3  13571  summolem3  13618  summolem2a  13619  fsumcl  13637  fsummulc2  13681  fsumrelem  13703  binom  13724  isumsplit  13734  efcj  13909  ef4p  13930  tanval3  13951  efi4p  13954  sinadd  13981  cosadd  13982  tanadd  13984  addsin  13987  demoivreALT  14018  opoe  14419  pythagtriplem4  14427  pythagtriplem12  14434  pythagtriplem14  14436  pythagtriplem16  14438  gzaddcl  14539  cnaddablx  17073  cnaddabl  17074  cncrng  18634  cnperf  21491  dvaddbr  22507  dvaddf  22511  dveflem  22546  plyaddcl  22783  plymulcl  22784  plysubcl  22785  coeaddlem  22812  dgrcolem1  22836  dgrcolem2  22837  quotlem  22862  quotcl2  22864  quotdgr  22865  sinperlem  23039  ptolemy  23055  tangtx  23064  sinkpi  23078  efif1olem2  23096  logrnaddcl  23128  logneg  23141  logimul  23167  cxpadd  23228  binom4  23378  atanf  23408  atanneg  23435  atancj  23438  efiatan  23440  atanlogaddlem  23441  atanlogadd  23442  atanlogsublem  23443  atanlogsub  23444  efiatan2  23445  2efiatan  23446  tanatan  23447  cosatan  23449  cosatanne0  23450  atantan  23451  atanbndlem  23453  atans2  23459  dvatan  23463  atantayl  23465  efrlim  23497  dfef2  23498  ftalem7  23550  prmorcht  23650  bposlem9  23765  lgsquad2lem1  23831  2sqlem2  23837  wlkdvspthlem  24811  wwlkext2clwwlk  25005  gxadd  25475  cncph  25932  hhssnv  26378  hoadddir  26921  superpos  27471  gamcvg2lem  28865  risefacval2  29373  risefaccl  29378  risefallfac  29387  risefacp1  29392  binomfallfac  29404  binomrisefac  29405  bpoly3  30048  cos2h  30286  tan2h  30287  dvtanlem  30304  ftc1anclem3  30332  ftc1anclem7  30336  ftc1anclem8  30337  ftc1anc  30338  stirlinglem5  32099  stirlinglem7  32101  opoeALTV  32589  cnapbmcpd  32690
  Copyright terms: Public domain W3C validator