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

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

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 10586 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  (class class class)co 7148  cc 10524   + caddc 10529
This theorem was proved from axioms:  ax-addcl 10586
This theorem is referenced by:  adddir  10621  0cn  10622  addcli  10636  addcld  10649  muladd11  10799  peano2cn  10801  muladd11r  10842  add4  10849  0cnALT2  10864  negeu  10865  pncan  10881  2addsub  10889  addsubeq4  10890  nppcan2  10906  pnpcan  10914  ppncan  10917  muladd  11061  mulsub  11072  recex  11261  muleqadd  11273  conjmul  11346  halfaddsubcl  11858  halfaddsub  11859  serf  13388  seradd  13402  sersub  13403  binom3  13575  bernneq  13580  lswccatn0lsw  13935  revccat  14118  2cshwcshw  14177  shftlem  14417  shftval2  14424  shftval5  14427  2shfti  14429  crre  14463  crim  14464  cjadd  14490  addcj  14497  sqabsadd  14632  absreimsq  14642  absreim  14643  abstri  14680  sqreulem  14709  sqreu  14710  addcn2  14940  o1add  14960  climadd  14978  clim2ser  15001  clim2ser2  15002  isermulc2  15004  isercolllem3  15013  summolem3  15061  summolem2a  15062  fsumcl  15080  fsummulc2  15129  fsumrelem  15152  binom  15175  isumsplit  15185  risefacval2  15354  risefaccl  15359  risefallfac  15368  risefacp1  15373  binomfallfac  15385  binomrisefac  15386  bpoly3  15402  efcj  15435  ef4p  15456  tanval3  15477  efi4p  15480  sinadd  15507  cosadd  15508  tanadd  15510  addsin  15513  demoivreALT  15544  opoe  15702  pythagtriplem4  16146  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem16  16157  gzaddcl  16263  cnaddablx  18908  cnaddabl  18909  cncrng  20482  cnperf  23343  cnlmod  23659  cnstrcvs  23660  cncvs  23664  dvaddbr  24450  dvaddf  24454  dveflem  24491  plyaddcl  24725  plymulcl  24726  plysubcl  24727  coeaddlem  24754  dgrcolem1  24778  dgrcolem2  24779  quotlem  24804  quotcl2  24806  quotdgr  24807  sinperlem  24981  ptolemy  24997  tangtx  25006  sinkpi  25022  efif1olem2  25040  logrnaddcl  25071  logneg  25084  logimul  25110  cxpadd  25175  binom4  25341  atanf  25371  atanneg  25398  atancj  25401  efiatan  25403  atanlogaddlem  25404  atanlogadd  25405  atanlogsublem  25406  atanlogsub  25407  efiatan2  25408  2efiatan  25409  tanatan  25410  cosatan  25412  cosatanne0  25413  atantan  25414  atanbndlem  25416  atans2  25422  dvatan  25426  atantayl  25428  efrlim  25461  dfef2  25462  gamcvg2lem  25550  ftalem7  25570  prmorcht  25669  bposlem9  25782  lgsquad2lem1  25874  2sqlem2  25908  cncph  28510  hhssnv  28955  hoadddir  29495  superpos  30045  knoppcnlem8  33723  cos2h  34750  tan2h  34751  ftc1anclem3  34836  ftc1anclem7  34840  ftc1anclem8  34841  ftc1anc  34842  fsumsermpt  41725  stirlinglem5  42229  stirlinglem7  42231  cnapbmcpd  43361  fmtnodvds  43538  opoeALTV  43680  mogoldbblem  43717
  Copyright terms: Public domain W3C validator