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

Theorem addcld 6824
Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  CC
addcld.2  CC
Assertion
Ref Expression
addcld  +  CC

Proof of Theorem addcld
StepHypRef Expression
1 addcld.1 . 2  CC
2 addcld.2 . 2  CC
3 addcl 6784 . 2  CC  CC  +  CC
41, 2, 3syl2anc 391 1  +  CC
Colors of variables: wff set class
Syntax hints:   wi 4   wcel 1390  (class class class)co 5455   CCcc 6689    + caddc 6694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addcl 6759
This theorem is referenced by:  negeu  6979  addsubass  6998  subsub2  7015  subsub4  7020  pnpcan  7026  pnncan  7028  addsub4  7030  apreim  7367  addext  7374  divdirap  7436  recp1lt1  7626  cju  7674  cnref1o  8337  expaddzap  8933  binom2  8995  binom3  8999  reval  9057  imval  9058  crre  9065  remullem  9079  imval2  9102  cjreim2  9112  cnrecnv  9118
  Copyright terms: Public domain W3C validator