Theorem addcld 7785

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 7745	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 408	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1480  (class class class)co 5774  ℂcc 7618   + caddc 7623

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

This theorem is referenced by:  muladd11r  7918  negeu  7953  addsubass  7972  subsub2  7990  subsub4  7995  pnpcan  8001  pnncan  8003  addsub4  8005  pnpncand  8137  apreim  8365  addext  8372  aprcl  8408  divdirap  8457  recp1lt1  8657  cju  8719  cnref1o  9440  modsumfzodifsn  10169  expaddzap  10337  binom2  10403  binom3  10409  sqoddm1div8  10444  nn0opthlem1d  10466  reval  10621  imval  10622  crre  10629  remullem  10643  imval2  10666  cjreim2  10676  cnrecnv  10682  resqrexlemcalc1  10786  maxabslemab  10978  maxltsup  10990  max0addsup  10991  minabs  11007  bdtrilem  11010  bdtri  11011  addcn2  11079  fsumadd  11175  isumadd  11200  binomlem  11252  efaddlem  11380  ef4p  11400  cosval  11410  cosf  11412  tanval2ap  11420  tanval3ap  11421  resin4p  11425  recos4p  11426  efival  11439  sinadd  11443  cosadd  11444  tanaddap  11446  oddennn  11905  addccncf  12755  limcimolemlt  12802  dvaddxxbr  12834  ptolemy  12905  qdencn  13222