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

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (φ → A ∈ ℂ)
2		addcld.2	. 2 ⊢ (φ → B ∈ ℂ)
3		addcl 6804	. 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 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