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

Theorem addcld 7046
Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
addcld  |-  ( ph  ->  ( A  +  B
)  e.  CC )

Proof of Theorem addcld
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addcl 7006 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3syl2anc 391 1  |-  ( ph  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1393  (class class class)co 5512   CCcc 6887    + caddc 6892
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addcl 6980
This theorem is referenced by:  negeu  7202  addsubass  7221  subsub2  7239  subsub4  7244  pnpcan  7250  pnncan  7252  addsub4  7254  apreim  7594  addext  7601  divdirap  7674  recp1lt1  7865  cju  7913  cnref1o  8582  expaddzap  9299  binom2  9362  binom3  9366  reval  9449  imval  9450  crre  9457  remullem  9471  imval2  9494  cjreim2  9504  cnrecnv  9510  resqrexlemcalc1  9612  addcn2  9831  qdencn  10124
  Copyright terms: Public domain W3C validator