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

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

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 7420 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1438  (class class class)co 5634  cc 7327   + caddc 7332
This theorem was proved from axioms:  ax-addcl 7420
This theorem is referenced by:  adddir  7458  0cn  7459  addcli  7471  addcld  7486  muladd11  7594  peano2cn  7596  muladd11r  7617  add4  7622  cnegexlem3  7638  cnegex  7639  0cnALT  7651  negeu  7652  pncan  7667  2addsub  7675  addsubeq4  7676  nppcan2  7692  ppncan  7703  muladd  7841  mulsub  7858  recexap  8096  muleqadd  8111  conjmulap  8170  halfaddsubcl  8619  halfaddsub  8620  serf  9865  iseqseq3  9867  iserf  9868  iseradd  9899  isersub  9901  iser0  9912  ser0  9914  binom2  10030  binom3  10036  bernneq  10039  shftlem  10215  shftval2  10225  shftval5  10228  2shfti  10230  crre  10256  crim  10257  cjadd  10283  addcj  10290  sqabsadd  10453  absreimsq  10465  absreim  10466  abstri  10502  addcn2  10663  climadd  10678  clim2ser  10689  clim2ser2  10690  iisermulc2  10692  serif0  10705  isumrblem  10729  fisumcvg  10730  fsum3cvg  10731  isummolem3  10734  isummolem2a  10735  zisum  10738  fisum  10742  fisumcvg2  10750  fisumser  10753  fsumcl2lem  10755  fsumcl  10757  sumsnf  10766  fsummulc2  10805  binom  10840  isumshft  10846  isumsplit  10847  geolim2  10867  cvgratnnlemseq  10881  cvgratz  10887  opoe  10988
  Copyright terms: Public domain W3C validator