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

Theorem addcld 7104
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 7064 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3syl2anc 397 1  |-  ( ph  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1409  (class class class)co 5540   CCcc 6945    + caddc 6950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105  ax-addcl 7038
This theorem is referenced by:  muladd11r  7230  negeu  7265  addsubass  7284  subsub2  7302  subsub4  7307  pnpcan  7313  pnncan  7315  addsub4  7317  pnpncand  7445  apreim  7668  addext  7675  divdirap  7748  recp1lt1  7940  cju  7989  cnref1o  8680  modsumfzodifsn  9346  expaddzap  9464  binom2  9529  binom3  9534  sqoddm1div8  9569  nn0opthlem1d  9588  reval  9677  imval  9678  crre  9685  remullem  9699  imval2  9722  cjreim2  9732  cnrecnv  9738  resqrexlemcalc1  9841  addcn2  10062  qdencn  10511
  Copyright terms: Public domain W3C validator