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

Theorem addcl 9572
Description: Alias for ax-addcl 9550, for naming consistency with addcli 9598. Use this theorem instead of ax-addcl 9550 or axaddcl 9526. (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 9550 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 1802  (class class class)co 6277   CCcc 9488    + caddc 9493
This theorem was proved from axioms:  ax-addcl 9550
This theorem is referenced by:  adddir  9585  0cn  9586  addcli  9598  addcld  9613  muladd11  9748  peano2cn  9750  add4  9794  0cnALT  9809  negeu  9810  pncan  9826  2addsub  9834  addsubeq4  9835  nppcan2  9850  ppncan  9861  muladd  9990  mulsub  10000  recex  10182  muleqadd  10194  conjmul  10262  halfaddsubcl  10772  halfaddsub  10773  uzindOLD  10958  serf  12109  seradd  12123  sersub  12124  binom3  12261  bernneq  12266  lswccatn0lsw  12581  revccat  12714  2cshwcshw  12767  shftlem  12875  shftval2  12882  shftval5  12885  2shfti  12887  crre  12921  crim  12922  cjadd  12948  addcj  12955  sqabsadd  13089  absreimsq  13099  absreim  13100  abstri  13137  sqreulem  13166  sqreu  13167  addcn2  13390  o1add  13410  climadd  13428  clim2ser  13451  clim2ser2  13452  isermulc2  13454  isercolllem3  13463  summolem3  13510  summolem2a  13511  fsumcl  13529  fsummulc2  13573  fsumrelem  13595  binom  13616  isumsplit  13626  efcj  13700  ef4p  13720  tanval3  13741  efi4p  13744  sinadd  13771  cosadd  13772  tanadd  13774  addsin  13777  demoivreALT  13808  opoe  14207  pythagtriplem4  14215  pythagtriplem12  14222  pythagtriplem14  14224  pythagtriplem16  14226  gzaddcl  14327  cnaddablx  16743  cnaddabl  16744  cncrng  18307  cnperf  21191  dvaddbr  22207  dvaddf  22211  dveflem  22246  plyaddcl  22483  plymulcl  22484  plysubcl  22485  coeaddlem  22511  dgrcolem1  22535  dgrcolem2  22536  quotlem  22561  quotcl2  22563  quotdgr  22564  sinperlem  22738  ptolemy  22754  tangtx  22763  sinkpi  22777  efif1olem2  22795  logrnaddcl  22827  logneg  22837  logimul  22864  cxpadd  22925  binom4  23046  atanf  23076  atanneg  23103  atancj  23106  efiatan  23108  atanlogaddlem  23109  atanlogadd  23110  atanlogsublem  23111  atanlogsub  23112  efiatan2  23113  2efiatan  23114  tanatan  23115  cosatan  23117  cosatanne0  23118  atantan  23119  atanbndlem  23121  atans2  23127  dvatan  23131  atantayl  23133  efrlim  23164  dfef2  23165  ftalem7  23217  prmorcht  23317  bposlem9  23432  lgsquad2lem1  23498  2sqlem2  23504  wlkdvspthlem  24474  wwlkext2clwwlk  24668  gxadd  25142  cncph  25599  hhssnv  26045  hoadddir  26588  superpos  27138  gamcvg2lem  28467  risefacval2  29100  risefaccl  29105  risefallfac  29114  risefacp1  29119  binomfallfac  29131  binomrisefac  29132  bpoly3  29788  cos2h  30014  tan2h  30015  dvtanlem  30032  ftc1anclem3  30060  ftc1anclem7  30064  ftc1anclem8  30065  ftc1anc  30066  stirlinglem5  31745  stirlinglem7  31747  cnapbmcpd  32150
  Copyright terms: Public domain W3C validator