Theorem addcld 8189

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6013  ℂcc 8020   + caddc 8025

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

This theorem is referenced by:  muladd11r  8325  negeu  8360  addsubass  8379  subsub2  8397  subsub4  8402  pnpcan  8408  pnncan  8410  addsub4  8412  pnpncand  8544  apreim  8773  addext  8780  aprcl  8816  aptap  8820  divdirap  8867  recp1lt1  9069  cju  9131  cnref1o  9875  modsumfzodifsn  10648  expaddzap  10835  binom2  10903  binom3  10909  sqoddm1div8  10945  mulsubdivbinom2ap  10963  nn0opthlem1d  10972  reval  11400  imval  11401  crre  11408  remullem  11422  imval2  11445  cjreim2  11455  cnrecnv  11461  resqrexlemcalc1  11565  maxabslemab  11757  maxltsup  11769  max0addsup  11770  minabs  11787  bdtrilem  11790  bdtri  11791  addcn2  11861  fsumadd  11957  isumadd  11982  binomlem  12034  efaddlem  12225  ef4p  12245  cosval  12254  cosf  12256  tanval2ap  12264  tanval3ap  12265  resin4p  12269  recos4p  12270  efival  12283  sinadd  12287  cosadd  12288  tanaddap  12290  pythagtriplem1  12828  pythagtriplem12  12838  pythagtriplem16  12842  pythagtriplem17  12843  pcbc  12914  mul4sqlem  12956  4sqlem14  12967  oddennn  13003  mulgdirlem  13730  gsumfzconst  13918  gsumfzfsumlemm  14591  addccncf  15314  limcimolemlt  15378  dvaddxxbr  15415  plyaddlem1  15461  ptolemy  15538  rpcxpadd  15619  binom4  15693  lgsquad2lem1  15800  2lgslem3d1  15819  qdencn  16567  iooref1o  16574  apdifflemr  16587