Theorem addcld 7979

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

Syntax hints:   → wi 4   ∈ wcel 2148  (class class class)co 5877  ℂcc 7811   + caddc 7816

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

This theorem is referenced by:  muladd11r  8115  negeu  8150  addsubass  8169  subsub2  8187  subsub4  8192  pnpcan  8198  pnncan  8200  addsub4  8202  pnpncand  8334  apreim  8562  addext  8569  aprcl  8605  aptap  8609  divdirap  8656  recp1lt1  8858  cju  8920  cnref1o  9652  modsumfzodifsn  10398  expaddzap  10566  binom2  10634  binom3  10640  sqoddm1div8  10676  mulsubdivbinom2ap  10693  nn0opthlem1d  10702  reval  10860  imval  10861  crre  10868  remullem  10882  imval2  10905  cjreim2  10915  cnrecnv  10921  resqrexlemcalc1  11025  maxabslemab  11217  maxltsup  11229  max0addsup  11230  minabs  11246  bdtrilem  11249  bdtri  11250  addcn2  11320  fsumadd  11416  isumadd  11441  binomlem  11493  efaddlem  11684  ef4p  11704  cosval  11713  cosf  11715  tanval2ap  11723  tanval3ap  11724  resin4p  11728  recos4p  11729  efival  11742  sinadd  11746  cosadd  11747  tanaddap  11749  pythagtriplem1  12267  pythagtriplem12  12277  pythagtriplem16  12281  pythagtriplem17  12282  pcbc  12351  mul4sqlem  12393  oddennn  12395  mulgdirlem  13019  addccncf  14125  limcimolemlt  14172  dvaddxxbr  14204  ptolemy  14284  rpcxpadd  14365  binom4  14436  qdencn  14814  iooref1o  14821  apdifflemr  14834