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

Theorem addcl 7713
Description: Alias for ax-addcl 7684, for naming consistency with addcli 7738. Use this theorem instead of ax-addcl 7684 or axaddcl 7640. (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 7684 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 1465  (class class class)co 5742   CCcc 7586    + caddc 7591
This theorem was proved from axioms:  ax-addcl 7684
This theorem is referenced by:  adddir  7725  0cn  7726  addcli  7738  addcld  7753  muladd11  7863  peano2cn  7865  muladd11r  7886  add4  7891  cnegexlem3  7907  cnegex  7908  0cnALT  7920  negeu  7921  pncan  7936  2addsub  7944  addsubeq4  7945  nppcan2  7961  ppncan  7972  muladd  8114  mulsub  8131  recexap  8382  muleqadd  8397  conjmulap  8457  halfaddsubcl  8921  halfaddsub  8922  serf  10215  ser3add  10246  ser3sub  10247  ser0  10255  binom2  10371  binom3  10377  bernneq  10380  shftlem  10556  shftval2  10566  shftval5  10569  2shfti  10571  crre  10597  crim  10598  cjadd  10624  addcj  10631  sqabsadd  10795  absreimsq  10807  absreim  10808  abstri  10844  addcn2  11047  climadd  11063  clim2ser  11074  clim2ser2  11075  isermulc2  11077  serf0  11089  sumrbdclem  11113  fsum3cvg  11114  summodclem3  11117  summodclem2a  11118  zsumdc  11121  fsum3  11124  fsum3cvg2  11131  fsum3ser  11134  fsumcl2lem  11135  fsumcl  11137  sumsnf  11146  fsummulc2  11185  binom  11221  isumshft  11227  isumsplit  11228  geolim2  11249  cvgratnnlemseq  11263  cvgratz  11269  ef0lem  11293  efcj  11306  ef4p  11327  efgt1p  11329  tanval3ap  11348  efi4p  11351  sinadd  11370  cosadd  11371  tanaddap  11373  addsin  11376  demoivreALT  11407  opoe  11519  addccncf  12682  dvaddxxbr  12761  dvaddxx  12763  dviaddf  12765  dveflem  12782  sinperlem  12816  ptolemy  12832  tangtx  12846  sinkpi  12855
  Copyright terms: Public domain W3C validator