Theorem addcld 8065

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

Syntax hints:   → wi 4   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   + caddc 7901

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

This theorem is referenced by:  muladd11r  8201  negeu  8236  addsubass  8255  subsub2  8273  subsub4  8278  pnpcan  8284  pnncan  8286  addsub4  8288  pnpncand  8420  apreim  8649  addext  8656  aprcl  8692  aptap  8696  divdirap  8743  recp1lt1  8945  cju  9007  cnref1o  9744  modsumfzodifsn  10507  expaddzap  10694  binom2  10762  binom3  10768  sqoddm1div8  10804  mulsubdivbinom2ap  10822  nn0opthlem1d  10831  reval  11033  imval  11034  crre  11041  remullem  11055  imval2  11078  cjreim2  11088  cnrecnv  11094  resqrexlemcalc1  11198  maxabslemab  11390  maxltsup  11402  max0addsup  11403  minabs  11420  bdtrilem  11423  bdtri  11424  addcn2  11494  fsumadd  11590  isumadd  11615  binomlem  11667  efaddlem  11858  ef4p  11878  cosval  11887  cosf  11889  tanval2ap  11897  tanval3ap  11898  resin4p  11902  recos4p  11903  efival  11916  sinadd  11920  cosadd  11921  tanaddap  11923  pythagtriplem1  12461  pythagtriplem12  12471  pythagtriplem16  12475  pythagtriplem17  12476  pcbc  12547  mul4sqlem  12589  4sqlem14  12600  oddennn  12636  mulgdirlem  13361  gsumfzconst  13549  gsumfzfsumlemm  14221  addccncf  14944  limcimolemlt  15008  dvaddxxbr  15045  plyaddlem1  15091  ptolemy  15168  rpcxpadd  15249  binom4  15323  lgsquad2lem1  15430  2lgslem3d1  15449  qdencn  15784  iooref1o  15791  apdifflemr  15804