Theorem addcld 7809

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

Syntax hints:   → wi 4   ∈ wcel 1481  (class class class)co 5782  ℂcc 7642   + caddc 7647

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

This theorem is referenced by:  muladd11r  7942  negeu  7977  addsubass  7996  subsub2  8014  subsub4  8019  pnpcan  8025  pnncan  8027  addsub4  8029  pnpncand  8161  apreim  8389  addext  8396  aprcl  8432  divdirap  8481  recp1lt1  8681  cju  8743  cnref1o  9469  modsumfzodifsn  10200  expaddzap  10368  binom2  10434  binom3  10440  sqoddm1div8  10475  nn0opthlem1d  10498  reval  10653  imval  10654  crre  10661  remullem  10675  imval2  10698  cjreim2  10708  cnrecnv  10714  resqrexlemcalc1  10818  maxabslemab  11010  maxltsup  11022  max0addsup  11023  minabs  11039  bdtrilem  11042  bdtri  11043  addcn2  11111  fsumadd  11207  isumadd  11232  binomlem  11284  efaddlem  11417  ef4p  11437  cosval  11446  cosf  11448  tanval2ap  11456  tanval3ap  11457  resin4p  11461  recos4p  11462  efival  11475  sinadd  11479  cosadd  11480  tanaddap  11482  oddennn  11941  addccncf  12794  limcimolemlt  12841  dvaddxxbr  12873  ptolemy  12953  rpcxpadd  13034  qdencn  13397  apdifflemr  13415  iooref1o  13426