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

Theorem addcl 9062
Description: Alias for ax-addcl 9040, for naming consistency with addcli 9084. Use this theorem instead of ax-addcl 9040 or axaddcl 9016. (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 9040 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725  (class class class)co 6073   CCcc 8978    + caddc 8983
This theorem is referenced by:  adddir  9073  0cn  9074  addcli  9084  addcld  9097  muladd11  9226  peano2cn  9228  add4  9271  0cnALT  9285  negeu  9286  pncan  9301  2addsub  9309  addsubeq4  9310  nppcan2  9322  ppncan  9333  muladd  9456  mulsub  9466  recex  9644  muleqadd  9656  conjmul  9721  halfaddsubcl  10190  halfaddsub  10191  uzindOLD  10354  serf  11341  seradd  11355  sersub  11356  binom3  11490  bernneq  11495  revccat  11788  shftlem  11873  shftval2  11880  shftval5  11883  2shfti  11885  crre  11909  crim  11910  cjadd  11936  addcj  11943  sqabsadd  12077  absreimsq  12087  absreim  12088  abstri  12124  sqreulem  12153  sqreu  12154  addcn2  12377  o1add  12397  climadd  12415  clim2ser  12438  clim2ser2  12439  isermulc2  12441  isercolllem3  12450  summolem3  12498  summolem2a  12499  fsumcl  12517  fsummulc2  12557  fsumrelem  12576  binom  12599  isumsplit  12610  efcj  12684  ef4p  12704  tanval3  12725  efi4p  12728  sinadd  12755  cosadd  12756  tanadd  12758  addsin  12761  demoivreALT  12792  opoe  13175  pythagtriplem4  13183  pythagtriplem12  13190  pythagtriplem14  13192  pythagtriplem16  13194  gzaddcl  13295  cnaddablx  15471  cnaddabl  15472  cncrng  16712  cnperf  18841  dvaddbr  19814  dvaddf  19818  dveflem  19853  plyaddcl  20129  plymulcl  20130  plysubcl  20131  coeaddlem  20157  dgrcolem1  20181  dgrcolem2  20182  quotlem  20207  quotcl2  20209  quotdgr  20210  sinperlem  20378  ptolemy  20394  tangtx  20403  sinkpi  20417  efgh  20433  efif1olem2  20435  logrnaddcl  20462  logneg  20472  logimul  20499  cxpadd  20560  binom4  20680  atanf  20710  atanneg  20737  atancj  20740  efiatan  20742  atanlogaddlem  20743  atanlogadd  20744  atanlogsublem  20745  atanlogsub  20746  efiatan2  20747  2efiatan  20748  tanatan  20749  cosatan  20751  cosatanne0  20752  atantan  20753  atanbndlem  20755  atans2  20761  dvatan  20765  atantayl  20767  efrlim  20798  dfef2  20799  ftalem7  20851  prmorcht  20951  bposlem9  21066  lgsquad2lem1  21132  2sqlem2  21138  wlkdvspthlem  21597  gxadd  21853  cncph  22310  hhssnv  22754  hoadddir  23297  superpos  23847  gamcvg2lem  24833  risefacval2  25316  risefaccl  25321  risefallfac  25330  risefacp1  25335  binomfallfac  25347  binomrisefac  25348  bpoly3  26069  stirlinglem5  27758  stirlinglem7  27760  cshwidxn  28177
This theorem was proved from axioms:  ax-addcl 9040
  Copyright terms: Public domain W3C validator