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

Theorem addcl 8835
Description: Alias for ax-addcl 8813, for naming consistency with addcli 8857. Use this theorem instead of ax-addcl 8813 or axaddcl 8789. (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 8813 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696  (class class class)co 5874   CCcc 8751    + caddc 8756
This theorem is referenced by:  adddir  8846  0cn  8847  addcli  8857  addcld  8870  muladd11  8998  peano2cn  9000  add4  9043  0cnALT  9057  negeu  9058  pncan  9073  2addsub  9081  addsubeq4  9082  nppcan2  9094  ppncan  9105  muladd  9228  mulsub  9238  recex  9416  muleqadd  9428  conjmul  9493  halfaddsubcl  9960  halfaddsub  9961  uzindOLD  10122  serf  11090  seradd  11104  sersub  11105  binom3  11238  bernneq  11243  revccat  11500  shftlem  11579  shftval2  11586  shftval5  11589  2shfti  11591  crre  11615  crim  11616  cjadd  11642  addcj  11649  sqabsadd  11783  absreimsq  11793  absreim  11794  abstri  11830  sqreulem  11859  sqreu  11860  addcn2  12083  o1add  12103  climadd  12121  clim2ser  12144  clim2ser2  12145  isermulc2  12147  isercolllem3  12156  summolem3  12203  summolem2a  12204  fsumcl  12222  fsummulc2  12262  fsumrelem  12281  binom  12304  isumsplit  12315  efcj  12389  ef4p  12409  tanval3  12430  efi4p  12433  sinadd  12460  cosadd  12461  tanadd  12463  addsin  12466  demoivreALT  12497  opoe  12880  pythagtriplem4  12888  pythagtriplem12  12895  pythagtriplem14  12897  pythagtriplem16  12899  gzaddcl  13000  cnaddablx  15174  cnaddabl  15175  cncrng  16411  cnperf  18341  dvaddbr  19303  dvaddf  19307  dveflem  19342  plyaddcl  19618  plymulcl  19619  plysubcl  19620  coeaddlem  19646  dgrcolem1  19670  dgrcolem2  19671  quotlem  19696  quotcl2  19698  quotdgr  19699  sinperlem  19864  ptolemy  19880  tangtx  19889  sinkpi  19903  efgh  19919  efif1olem2  19921  logrnaddcl  19947  logneg  19957  logimul  19984  cxpadd  20042  binom4  20162  atanf  20192  atanneg  20219  atancj  20222  efiatan  20224  atanlogaddlem  20225  atanlogadd  20226  atanlogsublem  20227  atanlogsub  20228  efiatan2  20229  2efiatan  20230  tanatan  20231  cosatan  20233  cosatanne0  20234  atantan  20235  atanbndlem  20237  atans2  20243  dvatan  20247  atantayl  20249  efrlim  20280  dfef2  20281  ftalem7  20332  prmorcht  20432  bposlem9  20547  lgsquad2lem1  20613  2sqlem2  20619  gxadd  20958  cncph  21413  hhssnv  21857  hoadddir  22400  superpos  22950  dmgmseqn0  23711  bpoly3  24864  fsumcube  24866  2wsms  25710  lvsovso  25728  sigadd  25751  distsava  25791  stoweidlem1  27852  stoweidlem11  27862  stoweidlem13  27864  stirlinglem5  27929  stirlinglem7  27931  wlkdvspthlem  28364
This theorem was proved from axioms:  ax-addcl 8813
  Copyright terms: Public domain W3C validator