Theorem addcld 8074

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

Syntax hints:   → wi 4   ∈ wcel 2175  (class class class)co 5934  ℂcc 7905   + caddc 7910

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

This theorem is referenced by:  muladd11r  8210  negeu  8245  addsubass  8264  subsub2  8282  subsub4  8287  pnpcan  8293  pnncan  8295  addsub4  8297  pnpncand  8429  apreim  8658  addext  8665  aprcl  8701  aptap  8705  divdirap  8752  recp1lt1  8954  cju  9016  cnref1o  9754  modsumfzodifsn  10522  expaddzap  10709  binom2  10777  binom3  10783  sqoddm1div8  10819  mulsubdivbinom2ap  10837  nn0opthlem1d  10846  reval  11079  imval  11080  crre  11087  remullem  11101  imval2  11124  cjreim2  11134  cnrecnv  11140  resqrexlemcalc1  11244  maxabslemab  11436  maxltsup  11448  max0addsup  11449  minabs  11466  bdtrilem  11469  bdtri  11470  addcn2  11540  fsumadd  11636  isumadd  11661  binomlem  11713  efaddlem  11904  ef4p  11924  cosval  11933  cosf  11935  tanval2ap  11943  tanval3ap  11944  resin4p  11948  recos4p  11949  efival  11962  sinadd  11966  cosadd  11967  tanaddap  11969  pythagtriplem1  12507  pythagtriplem12  12517  pythagtriplem16  12521  pythagtriplem17  12522  pcbc  12593  mul4sqlem  12635  4sqlem14  12646  oddennn  12682  mulgdirlem  13407  gsumfzconst  13595  gsumfzfsumlemm  14267  addccncf  14990  limcimolemlt  15054  dvaddxxbr  15091  plyaddlem1  15137  ptolemy  15214  rpcxpadd  15295  binom4  15369  lgsquad2lem1  15476  2lgslem3d1  15495  qdencn  15830  iooref1o  15837  apdifflemr  15850