Theorem addcld 8091

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

Syntax hints:   → wi 4   ∈ wcel 2175  (class class class)co 5943  ℂcc 7922   + caddc 7927

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

This theorem is referenced by:  muladd11r  8227  negeu  8262  addsubass  8281  subsub2  8299  subsub4  8304  pnpcan  8310  pnncan  8312  addsub4  8314  pnpncand  8446  apreim  8675  addext  8682  aprcl  8718  aptap  8722  divdirap  8769  recp1lt1  8971  cju  9033  cnref1o  9771  modsumfzodifsn  10539  expaddzap  10726  binom2  10794  binom3  10800  sqoddm1div8  10836  mulsubdivbinom2ap  10854  nn0opthlem1d  10863  reval  11102  imval  11103  crre  11110  remullem  11124  imval2  11147  cjreim2  11157  cnrecnv  11163  resqrexlemcalc1  11267  maxabslemab  11459  maxltsup  11471  max0addsup  11472  minabs  11489  bdtrilem  11492  bdtri  11493  addcn2  11563  fsumadd  11659  isumadd  11684  binomlem  11736  efaddlem  11927  ef4p  11947  cosval  11956  cosf  11958  tanval2ap  11966  tanval3ap  11967  resin4p  11971  recos4p  11972  efival  11985  sinadd  11989  cosadd  11990  tanaddap  11992  pythagtriplem1  12530  pythagtriplem12  12540  pythagtriplem16  12544  pythagtriplem17  12545  pcbc  12616  mul4sqlem  12658  4sqlem14  12669  oddennn  12705  mulgdirlem  13431  gsumfzconst  13619  gsumfzfsumlemm  14291  addccncf  15014  limcimolemlt  15078  dvaddxxbr  15115  plyaddlem1  15161  ptolemy  15238  rpcxpadd  15319  binom4  15393  lgsquad2lem1  15500  2lgslem3d1  15519  qdencn  15899  iooref1o  15906  apdifflemr  15919