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

Theorem addcl 7212
Description: Alias for ax-addcl 7186, for naming consistency with addcli 7237. Use this theorem instead of ax-addcl 7186 or axaddcl 7146. (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 7186 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1434  (class class class)co 5563   CCcc 7093    + caddc 7098
This theorem was proved from axioms:  ax-addcl 7186
This theorem is referenced by:  adddir  7224  0cn  7225  addcli  7237  addcld  7252  muladd11  7360  peano2cn  7362  muladd11r  7383  add4  7388  cnegexlem3  7404  cnegex  7405  0cnALT  7417  negeu  7418  pncan  7433  2addsub  7441  addsubeq4  7442  nppcan2  7458  ppncan  7469  muladd  7607  mulsub  7624  recexap  7862  muleqadd  7877  conjmulap  7936  halfaddsubcl  8383  halfaddsub  8384  iserf  9601  iseradd  9611  isersub  9612  iser0  9620  serige0  9622  serile  9623  binom2  9734  binom3  9739  bernneq  9742  shftlem  9905  shftval2  9915  shftval5  9918  2shfti  9920  crre  9945  crim  9946  cjadd  9972  addcj  9979  sqabsadd  10142  absreimsq  10154  absreim  10155  abstri  10191  addcn2  10350  climadd  10365  clim2iser  10376  clim2iser2  10377  iisermulc2  10379  iserile  10381  climserile  10384  serif0  10390  isumrblem  10400  fisumcvg  10401  opoe  10502
  Copyright terms: Public domain W3C validator