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

Theorem addcl 7757
Description: Alias for ax-addcl 7728, for naming consistency with addcli 7782. Use this theorem instead of ax-addcl 7728 or axaddcl 7684. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addcl  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 7728 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1480  (class class class)co 5774   CCcc 7630    + caddc 7635
This theorem was proved from axioms:  ax-addcl 7728
This theorem is referenced by:  adddir  7769  0cn  7770  addcli  7782  addcld  7797  muladd11  7907  peano2cn  7909  muladd11r  7930  add4  7935  cnegexlem3  7951  cnegex  7952  0cnALT  7964  negeu  7965  pncan  7980  2addsub  7988  addsubeq4  7989  nppcan2  8005  ppncan  8016  muladd  8158  mulsub  8175  recexap  8426  muleqadd  8441  conjmulap  8501  halfaddsubcl  8965  halfaddsub  8966  serf  10259  ser3add  10290  ser3sub  10291  ser0  10299  binom2  10415  binom3  10421  bernneq  10424  shftlem  10600  shftval2  10610  shftval5  10613  2shfti  10615  crre  10641  crim  10642  cjadd  10668  addcj  10675  sqabsadd  10839  absreimsq  10851  absreim  10852  abstri  10888  addcn2  11091  climadd  11107  clim2ser  11118  clim2ser2  11119  isermulc2  11121  serf0  11133  sumrbdclem  11158  fsum3cvg  11159  summodclem3  11161  summodclem2a  11162  zsumdc  11165  fsum3  11168  fsum3cvg2  11175  fsum3ser  11178  fsumcl2lem  11179  fsumcl  11181  sumsnf  11190  fsummulc2  11229  binom  11265  isumshft  11271  isumsplit  11272  geolim2  11293  cvgratnnlemseq  11307  cvgratz  11313  ef0lem  11378  efcj  11391  ef4p  11412  efgt1p  11414  tanval3ap  11432  efi4p  11435  sinadd  11454  cosadd  11455  tanaddap  11457  addsin  11460  demoivreALT  11491  opoe  11603  addccncf  12769  dvaddxxbr  12848  dvaddxx  12850  dviaddf  12852  dveflem  12870  sinperlem  12911  ptolemy  12927  tangtx  12941  sinkpi  12950
  Copyright terms: Public domain W3C validator