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

Theorem addcld 6804
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 6764 . 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 6669   + caddc 6674
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addcl 6739
This theorem is referenced by:  negeu  6959  addsubass  6978  subsub2  6995  subsub4  7000  pnpcan  7006  pnncan  7008  addsub4  7010  apreim  7347  addext  7354  divdirap  7416  recp1lt1  7606  cju  7654  cnref1o  8317  expaddzap  8913  binom2  8975  binom3  8979  reval  9037  imval  9038  crre  9045  remullem  9059  imval2  9082  cjreim2  9092  cnrecnv  9098
  Copyright terms: Public domain W3C validator