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

Theorem addcld 6844
Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (φA ℂ)
addcld.2 (φB ℂ)
Assertion
Ref Expression
addcld (φ → (A + B) ℂ)

Proof of Theorem addcld
StepHypRef Expression
1 addcld.1 . 2 (φA ℂ)
2 addcld.2 . 2 (φB ℂ)
3 addcl 6804 . 2 ((A B ℂ) → (A + B) ℂ)
41, 2, 3syl2anc 391 1 (φ → (A + B) ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  (class class class)co 5455  cc 6709   + caddc 6714
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addcl 6779
This theorem is referenced by:  negeu  6999  addsubass  7018  subsub2  7035  subsub4  7040  pnpcan  7046  pnncan  7048  addsub4  7050  apreim  7387  addext  7394  divdirap  7456  recp1lt1  7646  cju  7694  cnref1o  8357  expaddzap  8953  binom2  9015  binom3  9019  reval  9077  imval  9078  crre  9085  remullem  9099  imval2  9122  cjreim2  9132  cnrecnv  9138
  Copyright terms: Public domain W3C validator