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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (φ → A ∈ ℂ)
2		addcld.2	. 2 ⊢ (φ → B ∈ ℂ)
3		addcl 6764	. 2 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A + B) ∈ ℂ)
4	1, 2, 3	syl2anc 391	1 ⊢ (φ → (A + B) ∈ ℂ)

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