Theorem addcld 8199

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   + caddc 8035

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

This theorem is referenced by:  muladd11r  8335  negeu  8370  addsubass  8389  subsub2  8407  subsub4  8412  pnpcan  8418  pnncan  8420  addsub4  8422  pnpncand  8554  apreim  8783  addext  8790  aprcl  8826  aptap  8830  divdirap  8877  recp1lt1  9079  cju  9141  cnref1o  9885  modsumfzodifsn  10659  expaddzap  10846  binom2  10914  binom3  10920  sqoddm1div8  10956  mulsubdivbinom2ap  10974  nn0opthlem1d  10983  reval  11414  imval  11415  crre  11422  remullem  11436  imval2  11459  cjreim2  11469  cnrecnv  11475  resqrexlemcalc1  11579  maxabslemab  11771  maxltsup  11783  max0addsup  11784  minabs  11801  bdtrilem  11804  bdtri  11805  addcn2  11875  fsumadd  11972  isumadd  11997  binomlem  12049  efaddlem  12240  ef4p  12260  cosval  12269  cosf  12271  tanval2ap  12279  tanval3ap  12280  resin4p  12284  recos4p  12285  efival  12298  sinadd  12302  cosadd  12303  tanaddap  12305  pythagtriplem1  12843  pythagtriplem12  12853  pythagtriplem16  12857  pythagtriplem17  12858  pcbc  12929  mul4sqlem  12971  4sqlem14  12982  oddennn  13018  mulgdirlem  13745  gsumfzconst  13933  gsumfzfsumlemm  14607  addccncf  15330  limcimolemlt  15394  dvaddxxbr  15431  plyaddlem1  15477  ptolemy  15554  rpcxpadd  15635  binom4  15709  lgsquad2lem1  15816  2lgslem3d1  15835  qdencn  16657  iooref1o  16664  apdifflemr  16677  qdiff  16679