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

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

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 10249 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2155  (class class class)co 6842  cc 10187   + caddc 10192
This theorem was proved from axioms:  ax-addcl 10249
This theorem is referenced by:  adddir  10284  0cn  10285  addcli  10300  addcld  10313  muladd11  10460  peano2cn  10462  muladd11r  10503  add4  10510  0cnALT  10524  negeu  10525  pncan  10541  2addsub  10549  addsubeq4  10550  nppcan2  10566  ppncan  10577  muladd  10716  mulsub  10727  recex  10913  muleqadd  10925  conjmul  10996  halfaddsubcl  11510  halfaddsub  11511  serf  13036  seradd  13050  sersub  13051  binom3  13192  bernneq  13197  lswccatn0lsw  13562  revccat  13790  2cshwcshw  13854  shftlem  14093  shftval2  14100  shftval5  14103  2shfti  14105  crre  14139  crim  14140  cjadd  14166  addcj  14173  sqabsadd  14307  absreimsq  14317  absreim  14318  abstri  14355  sqreulem  14384  sqreu  14385  addcn2  14609  o1add  14629  climadd  14647  clim2ser  14670  clim2ser2  14671  isermulc2  14673  isercolllem3  14682  summolem3  14730  summolem2a  14731  fsumcl  14749  fsummulc2  14800  fsumrelem  14823  binom  14846  isumsplit  14856  risefacval2  15023  risefaccl  15028  risefallfac  15037  risefacp1  15042  binomfallfac  15054  binomrisefac  15055  bpoly3  15071  efcj  15104  ef4p  15125  tanval3  15146  efi4p  15149  sinadd  15176  cosadd  15177  tanadd  15179  addsin  15182  demoivreALT  15213  opoe  15369  pythagtriplem4  15803  pythagtriplem12  15810  pythagtriplem14  15812  pythagtriplem16  15814  gzaddcl  15920  cnaddablx  18537  cnaddabl  18538  cncrng  20040  cnperf  22902  cnlmod  23218  cnstrcvs  23219  cncvs  23223  dvaddbr  23992  dvaddf  23996  dveflem  24033  plyaddcl  24267  plymulcl  24268  plysubcl  24269  coeaddlem  24296  dgrcolem1  24320  dgrcolem2  24321  quotlem  24346  quotcl2  24348  quotdgr  24349  sinperlem  24524  ptolemy  24540  tangtx  24549  sinkpi  24563  efif1olem2  24581  logrnaddcl  24612  logneg  24625  logimul  24651  cxpadd  24716  binom4  24868  atanf  24898  atanneg  24925  atancj  24928  efiatan  24930  atanlogaddlem  24931  atanlogadd  24932  atanlogsublem  24933  atanlogsub  24934  efiatan2  24935  2efiatan  24936  tanatan  24937  cosatan  24939  cosatanne0  24940  atantan  24941  atanbndlem  24943  atans2  24949  dvatan  24953  atantayl  24955  efrlim  24987  dfef2  24988  gamcvg2lem  25076  ftalem7  25096  prmorcht  25195  bposlem9  25308  lgsquad2lem1  25400  2sqlem2  25434  wwlksext2clwwlkOLD  27308  cncph  28130  hhssnv  28577  hoadddir  29119  superpos  29669  knoppcnlem8  32929  cos2h  33824  tan2h  33825  ftc1anclem3  33910  ftc1anclem7  33914  ftc1anclem8  33915  ftc1anc  33916  fsumsermpt  40449  stirlinglem5  40932  stirlinglem7  40934  cnapbmcpd  42045  fmtnodvds  42132  opoeALTV  42270  mogoldbblem  42305
  Copyright terms: Public domain W3C validator