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

Theorem addcl 9573
Description: Alias for ax-addcl 9551, for naming consistency with addcli 9599. Use this theorem instead of ax-addcl 9551 or axaddcl 9527. (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 9551 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 1767  (class class class)co 6283   CCcc 9489    + caddc 9494
This theorem was proved from axioms:  ax-addcl 9551
This theorem is referenced by:  adddir  9586  0cn  9587  addcli  9599  addcld  9614  muladd11  9748  peano2cn  9750  add4  9794  0cnALT  9808  negeu  9809  pncan  9825  2addsub  9833  addsubeq4  9834  nppcan2  9849  ppncan  9860  muladd  9988  mulsub  9998  recex  10180  muleqadd  10192  conjmul  10260  halfaddsubcl  10770  halfaddsub  10771  uzindOLD  10954  serf  12102  seradd  12116  sersub  12117  binom3  12254  bernneq  12259  lswccatn0lsw  12570  revccat  12702  2cshwcshw  12755  shftlem  12863  shftval2  12870  shftval5  12873  2shfti  12875  crre  12909  crim  12910  cjadd  12936  addcj  12943  sqabsadd  13077  absreimsq  13087  absreim  13088  abstri  13125  sqreulem  13154  sqreu  13155  addcn2  13378  o1add  13398  climadd  13416  clim2ser  13439  clim2ser2  13440  isermulc2  13442  isercolllem3  13451  summolem3  13498  summolem2a  13499  fsumcl  13517  fsummulc2  13561  fsumrelem  13583  binom  13604  isumsplit  13614  efcj  13688  ef4p  13708  tanval3  13729  efi4p  13732  sinadd  13759  cosadd  13760  tanadd  13762  addsin  13765  demoivreALT  13796  opoe  14193  pythagtriplem4  14201  pythagtriplem12  14208  pythagtriplem14  14210  pythagtriplem16  14212  gzaddcl  14313  cnaddablx  16674  cnaddabl  16675  cncrng  18226  cnperf  21076  dvaddbr  22092  dvaddf  22096  dveflem  22131  plyaddcl  22368  plymulcl  22369  plysubcl  22370  coeaddlem  22396  dgrcolem1  22420  dgrcolem2  22421  quotlem  22446  quotcl2  22448  quotdgr  22449  sinperlem  22622  ptolemy  22638  tangtx  22647  sinkpi  22661  efgh  22677  efif1olem2  22679  logrnaddcl  22706  logneg  22716  logimul  22743  cxpadd  22804  binom4  22925  atanf  22955  atanneg  22982  atancj  22985  efiatan  22987  atanlogaddlem  22988  atanlogadd  22989  atanlogsublem  22990  atanlogsub  22991  efiatan2  22992  2efiatan  22993  tanatan  22994  cosatan  22996  cosatanne0  22997  atantan  22998  atanbndlem  23000  atans2  23006  dvatan  23010  atantayl  23012  efrlim  23043  dfef2  23044  ftalem7  23096  prmorcht  23196  bposlem9  23311  lgsquad2lem1  23377  2sqlem2  23383  wlkdvspthlem  24301  wwlkext2clwwlk  24495  gxadd  24969  cncph  25426  hhssnv  25872  hoadddir  26415  superpos  26965  gamcvg2lem  28257  risefacval2  28725  risefaccl  28730  risefallfac  28739  risefacp1  28744  binomfallfac  28756  binomrisefac  28757  bpoly3  29413  cos2h  29639  tan2h  29640  dvtanlem  29657  ftc1anclem3  29685  ftc1anclem7  29689  ftc1anclem8  29690  ftc1anc  29691  sumnnodd  31188  stirlinglem5  31394  stirlinglem7  31396  dirkerper  31412  dirkertrigeqlem3  31416  fourierdlem79  31502  fourierdlem112  31535  cnapbmcpd  31799
  Copyright terms: Public domain W3C validator