Theorem addcld 7926

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

Syntax hints:   → wi 4   ∈ wcel 2141  (class class class)co 5850  ℂcc 7759   + caddc 7764

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

This theorem is referenced by:  muladd11r  8062  negeu  8097  addsubass  8116  subsub2  8134  subsub4  8139  pnpcan  8145  pnncan  8147  addsub4  8149  pnpncand  8281  apreim  8509  addext  8516  aprcl  8552  divdirap  8601  recp1lt1  8802  cju  8864  cnref1o  9596  modsumfzodifsn  10339  expaddzap  10507  binom2  10574  binom3  10580  sqoddm1div8  10616  nn0opthlem1d  10641  reval  10800  imval  10801  crre  10808  remullem  10822  imval2  10845  cjreim2  10855  cnrecnv  10861  resqrexlemcalc1  10965  maxabslemab  11157  maxltsup  11169  max0addsup  11170  minabs  11186  bdtrilem  11189  bdtri  11190  addcn2  11260  fsumadd  11356  isumadd  11381  binomlem  11433  efaddlem  11624  ef4p  11644  cosval  11653  cosf  11655  tanval2ap  11663  tanval3ap  11664  resin4p  11668  recos4p  11669  efival  11682  sinadd  11686  cosadd  11687  tanaddap  11689  pythagtriplem1  12206  pythagtriplem12  12216  pythagtriplem16  12220  pythagtriplem17  12221  pcbc  12290  mul4sqlem  12332  oddennn  12334  addccncf  13301  limcimolemlt  13348  dvaddxxbr  13380  ptolemy  13460  rpcxpadd  13541  binom4  13612  qdencn  13981  iooref1o  13988  apdifflemr  14001