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

Theorem addcl 10607
Description: Alias for ax-addcl 10585, for naming consistency with addcli 10635. Use this theorem instead of ax-addcl 10585 or axaddcl 10561. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addcl ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 10585 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  (class class class)co 7145  cc 10523   + caddc 10528
This theorem was proved from axioms:  ax-addcl 10585
This theorem is referenced by:  adddir  10620  0cn  10621  addcli  10635  addcld  10648  muladd11  10798  peano2cn  10800  muladd11r  10841  add4  10848  0cnALT2  10863  negeu  10864  pncan  10880  2addsub  10888  addsubeq4  10889  nppcan2  10905  pnpcan  10913  ppncan  10916  muladd  11060  mulsub  11071  recex  11260  muleqadd  11272  conjmul  11345  halfaddsubcl  11857  halfaddsub  11858  serf  13386  seradd  13400  sersub  13401  binom3  13573  bernneq  13578  lswccatn0lsw  13933  revccat  14116  2cshwcshw  14175  shftlem  14415  shftval2  14422  shftval5  14425  2shfti  14427  crre  14461  crim  14462  cjadd  14488  addcj  14495  sqabsadd  14630  absreimsq  14640  absreim  14641  abstri  14678  sqreulem  14707  sqreu  14708  addcn2  14938  o1add  14958  climadd  14976  clim2ser  14999  clim2ser2  15000  isermulc2  15002  isercolllem3  15011  summolem3  15059  summolem2a  15060  fsumcl  15078  fsummulc2  15127  fsumrelem  15150  binom  15173  isumsplit  15183  risefacval2  15352  risefaccl  15357  risefallfac  15366  risefacp1  15371  binomfallfac  15383  binomrisefac  15384  bpoly3  15400  efcj  15433  ef4p  15454  tanval3  15475  efi4p  15478  sinadd  15505  cosadd  15506  tanadd  15508  addsin  15511  demoivreALT  15542  opoe  15700  pythagtriplem4  16144  pythagtriplem12  16151  pythagtriplem14  16153  pythagtriplem16  16155  gzaddcl  16261  cnaddablx  18917  cnaddabl  18918  cncrng  20494  cnperf  23355  cnlmod  23671  cnstrcvs  23672  cncvs  23676  dvaddbr  24462  dvaddf  24466  dveflem  24503  plyaddcl  24737  plymulcl  24738  plysubcl  24739  coeaddlem  24766  dgrcolem1  24790  dgrcolem2  24791  quotlem  24816  quotcl2  24818  quotdgr  24819  sinperlem  24993  ptolemy  25009  tangtx  25018  sinkpi  25034  efif1olem2  25054  logrnaddcl  25085  logneg  25098  logimul  25124  cxpadd  25189  binom4  25355  atanf  25385  atanneg  25412  atancj  25415  efiatan  25417  atanlogaddlem  25418  atanlogadd  25419  atanlogsublem  25420  atanlogsub  25421  efiatan2  25422  2efiatan  25423  tanatan  25424  cosatan  25426  cosatanne0  25427  atantan  25428  atanbndlem  25430  atans2  25436  dvatan  25440  atantayl  25442  efrlim  25474  dfef2  25475  gamcvg2lem  25563  ftalem7  25583  prmorcht  25682  bposlem9  25795  lgsquad2lem1  25887  2sqlem2  25921  cncph  28523  hhssnv  28968  hoadddir  29508  superpos  30058  knoppcnlem8  33736  cos2h  34764  tan2h  34765  ftc1anclem3  34850  ftc1anclem7  34854  ftc1anclem8  34855  ftc1anc  34856  fsumsermpt  41736  stirlinglem5  42240  stirlinglem7  42242  cnapbmcpd  43372  fmtnodvds  43583  opoeALTV  43725  mogoldbblem  43762
  Copyright terms: Public domain W3C validator