Theorem addcld 8002

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

Syntax hints:   → wi 4   ∈ wcel 2160  (class class class)co 5892  ℂcc 7834   + caddc 7839

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

This theorem is referenced by:  muladd11r  8138  negeu  8173  addsubass  8192  subsub2  8210  subsub4  8215  pnpcan  8221  pnncan  8223  addsub4  8225  pnpncand  8357  apreim  8585  addext  8592  aprcl  8628  aptap  8632  divdirap  8679  recp1lt1  8881  cju  8943  cnref1o  9675  modsumfzodifsn  10422  expaddzap  10590  binom2  10658  binom3  10664  sqoddm1div8  10700  mulsubdivbinom2ap  10718  nn0opthlem1d  10727  reval  10885  imval  10886  crre  10893  remullem  10907  imval2  10930  cjreim2  10940  cnrecnv  10946  resqrexlemcalc1  11050  maxabslemab  11242  maxltsup  11254  max0addsup  11255  minabs  11271  bdtrilem  11274  bdtri  11275  addcn2  11345  fsumadd  11441  isumadd  11466  binomlem  11518  efaddlem  11709  ef4p  11729  cosval  11738  cosf  11740  tanval2ap  11748  tanval3ap  11749  resin4p  11753  recos4p  11754  efival  11767  sinadd  11771  cosadd  11772  tanaddap  11774  pythagtriplem1  12292  pythagtriplem12  12302  pythagtriplem16  12306  pythagtriplem17  12307  pcbc  12378  mul4sqlem  12420  4sqlem14  12431  oddennn  12438  mulgdirlem  13086  addccncf  14523  limcimolemlt  14570  dvaddxxbr  14602  ptolemy  14682  rpcxpadd  14763  binom4  14834  qdencn  15213  iooref1o  15220  apdifflemr  15233