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

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

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 9849 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  (class class class)co 6524  cc 9787   + caddc 9792
This theorem was proved from axioms:  ax-addcl 9849
This theorem is referenced by:  adddir  9884  0cn  9885  addcli  9897  addcld  9912  muladd11  10054  peano2cn  10056  muladd11r  10097  add4  10104  0cnALT  10118  negeu  10119  pncan  10135  2addsub  10143  addsubeq4  10144  nppcan2  10160  ppncan  10171  muladd  10310  mulsub  10320  recex  10505  muleqadd  10517  conjmul  10588  halfaddsubcl  11108  halfaddsub  11109  serf  12643  seradd  12657  sersub  12658  binom3  12799  bernneq  12804  lswccatn0lsw  13169  revccat  13309  2cshwcshw  13365  shftlem  13599  shftval2  13606  shftval5  13609  2shfti  13611  crre  13645  crim  13646  cjadd  13672  addcj  13679  sqabsadd  13813  absreimsq  13823  absreim  13824  abstri  13861  sqreulem  13890  sqreu  13891  addcn2  14115  o1add  14135  climadd  14153  clim2ser  14176  clim2ser2  14177  isermulc2  14179  isercolllem3  14188  summolem3  14235  summolem2a  14236  fsumcl  14254  fsummulc2  14301  fsumrelem  14323  binom  14344  isumsplit  14354  risefacval2  14523  risefaccl  14528  risefallfac  14537  risefacp1  14542  binomfallfac  14554  binomrisefac  14555  bpoly3  14571  efcj  14604  ef4p  14625  tanval3  14646  efi4p  14649  sinadd  14676  cosadd  14677  tanadd  14679  addsin  14682  demoivreALT  14713  opoe  14868  pythagtriplem4  15305  pythagtriplem12  15312  pythagtriplem14  15314  pythagtriplem16  15316  gzaddcl  15422  cnaddablx  18037  cnaddabl  18038  cncrng  19529  cnperf  22360  cnlmod  22674  cnstrcvs  22675  cncvs  22679  dvaddbr  23421  dvaddf  23425  dveflem  23460  plyaddcl  23694  plymulcl  23695  plysubcl  23696  coeaddlem  23723  dgrcolem1  23747  dgrcolem2  23748  quotlem  23773  quotcl2  23775  quotdgr  23776  sinperlem  23950  ptolemy  23966  tangtx  23975  sinkpi  23989  efif1olem2  24007  logrnaddcl  24039  logneg  24052  logimul  24078  cxpadd  24139  binom4  24291  atanf  24321  atanneg  24348  atancj  24351  efiatan  24353  atanlogaddlem  24354  atanlogadd  24355  atanlogsublem  24356  atanlogsub  24357  efiatan2  24358  2efiatan  24359  tanatan  24360  cosatan  24362  cosatanne0  24363  atantan  24364  atanbndlem  24366  atans2  24372  dvatan  24376  atantayl  24378  efrlim  24410  dfef2  24411  gamcvg2lem  24499  ftalem7  24519  prmorcht  24618  bposlem9  24731  lgsquad2lem1  24823  2sqlem2  24857  wlkdvspthlem  25900  wwlkext2clwwlk  26094  cncph  26861  hhssnv  27308  hoadddir  27850  superpos  28400  knoppcnlem8  31463  cos2h  32370  tan2h  32371  ftc1anclem3  32457  ftc1anclem7  32461  ftc1anclem8  32462  ftc1anc  32463  fsumsermpt  38447  stirlinglem5  38772  stirlinglem7  38774  fmtnodvds  39796  opoeALTV  39934  cnapbmcpd  40166  wwlksext2clwwlk  41230
  Copyright terms: Public domain W3C validator