ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addcl GIF version

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

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 7735 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1480  (class class class)co 5777  cc 7637   + caddc 7642
This theorem was proved from axioms:  ax-addcl 7735
This theorem is referenced by:  adddir  7776  0cn  7777  addcli  7789  addcld  7804  muladd11  7914  peano2cn  7916  muladd11r  7937  add4  7942  cnegexlem3  7958  cnegex  7959  0cnALT  7971  negeu  7972  pncan  7987  2addsub  7995  addsubeq4  7996  nppcan2  8012  ppncan  8023  muladd  8165  mulsub  8182  recexap  8433  muleqadd  8448  conjmulap  8508  halfaddsubcl  8972  halfaddsub  8973  serf  10271  ser3add  10302  ser3sub  10303  ser0  10311  binom2  10427  binom3  10433  bernneq  10436  shftlem  10612  shftval2  10622  shftval5  10625  2shfti  10627  crre  10653  crim  10654  cjadd  10680  addcj  10687  sqabsadd  10851  absreimsq  10863  absreim  10864  abstri  10900  addcn2  11103  climadd  11119  clim2ser  11130  clim2ser2  11131  isermulc2  11133  serf0  11145  sumrbdclem  11170  fsum3cvg  11171  summodclem3  11173  summodclem2a  11174  zsumdc  11177  fsum3  11180  fsum3cvg2  11187  fsum3ser  11190  fsumcl2lem  11191  fsumcl  11193  sumsnf  11202  fsummulc2  11241  binom  11277  isumshft  11283  isumsplit  11284  geolim2  11305  cvgratnnlemseq  11319  cvgratz  11325  ef0lem  11390  efcj  11403  ef4p  11424  efgt1p  11426  tanval3ap  11444  efi4p  11447  sinadd  11466  cosadd  11467  tanaddap  11469  addsin  11472  demoivreALT  11503  opoe  11615  addccncf  12781  dvaddxxbr  12860  dvaddxx  12862  dviaddf  12864  dveflem  12882  sinperlem  12923  ptolemy  12939  tangtx  12953  sinkpi  12962
  Copyright terms: Public domain W3C validator