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

Theorem addcl 9007
Description: Alias for ax-addcl 8985, for naming consistency with addcli 9029. Use this theorem instead of ax-addcl 8985 or axaddcl 8961. (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 8985 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 1717  (class class class)co 6022   CCcc 8923    + caddc 8928
This theorem is referenced by:  adddir  9018  0cn  9019  addcli  9029  addcld  9042  muladd11  9170  peano2cn  9172  add4  9215  0cnALT  9229  negeu  9230  pncan  9245  2addsub  9253  addsubeq4  9254  nppcan2  9266  ppncan  9277  muladd  9400  mulsub  9410  recex  9588  muleqadd  9600  conjmul  9665  halfaddsubcl  10134  halfaddsub  10135  uzindOLD  10298  serf  11280  seradd  11294  sersub  11295  binom3  11429  bernneq  11434  revccat  11727  shftlem  11812  shftval2  11819  shftval5  11822  2shfti  11824  crre  11848  crim  11849  cjadd  11875  addcj  11882  sqabsadd  12016  absreimsq  12026  absreim  12027  abstri  12063  sqreulem  12092  sqreu  12093  addcn2  12316  o1add  12336  climadd  12354  clim2ser  12377  clim2ser2  12378  isermulc2  12380  isercolllem3  12389  summolem3  12437  summolem2a  12438  fsumcl  12456  fsummulc2  12496  fsumrelem  12515  binom  12538  isumsplit  12549  efcj  12623  ef4p  12643  tanval3  12664  efi4p  12667  sinadd  12694  cosadd  12695  tanadd  12697  addsin  12700  demoivreALT  12731  opoe  13114  pythagtriplem4  13122  pythagtriplem12  13129  pythagtriplem14  13131  pythagtriplem16  13133  gzaddcl  13234  cnaddablx  15410  cnaddabl  15411  cncrng  16647  cnperf  18724  dvaddbr  19693  dvaddf  19697  dveflem  19732  plyaddcl  20008  plymulcl  20009  plysubcl  20010  coeaddlem  20036  dgrcolem1  20060  dgrcolem2  20061  quotlem  20086  quotcl2  20088  quotdgr  20089  sinperlem  20257  ptolemy  20273  tangtx  20282  sinkpi  20296  efgh  20312  efif1olem2  20314  logrnaddcl  20341  logneg  20351  logimul  20378  cxpadd  20439  binom4  20559  atanf  20589  atanneg  20616  atancj  20619  efiatan  20621  atanlogaddlem  20622  atanlogadd  20623  atanlogsublem  20624  atanlogsub  20625  efiatan2  20626  2efiatan  20627  tanatan  20628  cosatan  20630  cosatanne0  20631  atantan  20632  atanbndlem  20634  atans2  20640  dvatan  20644  atantayl  20646  efrlim  20677  dfef2  20678  ftalem7  20730  prmorcht  20830  bposlem9  20945  lgsquad2lem1  21011  2sqlem2  21017  wlkdvspthlem  21457  gxadd  21713  cncph  22170  hhssnv  22614  hoadddir  23157  superpos  23707  gamcvg2lem  24624  risefacval2  25097  risefaccl  25101  risefallfac  25110  risefacp1  25115  bpoly3  25820  stirlinglem5  27497  stirlinglem7  27499
This theorem was proved from axioms:  ax-addcl 8985
  Copyright terms: Public domain W3C validator