Theorem addcld 7046

Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
addcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Proof of Theorem addcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addcl 7006	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 391	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1393  (class class class)co 5512  ℂcc 6887   + caddc 6892

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addcl 6980

This theorem is referenced by:  negeu  7202  addsubass  7221  subsub2  7239  subsub4  7244  pnpcan  7250  pnncan  7252  addsub4  7254  apreim  7594  addext  7601  divdirap  7674  recp1lt1  7865  cju  7913  cnref1o  8582  expaddzap  9299  binom2  9362  binom3  9366  reval  9449  imval  9450  crre  9457  remullem  9471  imval2  9494  cjreim2  9504  cnrecnv  9510  resqrexlemcalc1  9612  addcn2  9831  qdencn  10124