Theorem addcld 8063

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

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

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

This theorem is referenced by:  muladd11r  8199  negeu  8234  addsubass  8253  subsub2  8271  subsub4  8276  pnpcan  8282  pnncan  8284  addsub4  8286  pnpncand  8418  apreim  8647  addext  8654  aprcl  8690  aptap  8694  divdirap  8741  recp1lt1  8943  cju  9005  cnref1o  9742  modsumfzodifsn  10505  expaddzap  10692  binom2  10760  binom3  10766  sqoddm1div8  10802  mulsubdivbinom2ap  10820  nn0opthlem1d  10829  reval  11031  imval  11032  crre  11039  remullem  11053  imval2  11076  cjreim2  11086  cnrecnv  11092  resqrexlemcalc1  11196  maxabslemab  11388  maxltsup  11400  max0addsup  11401  minabs  11418  bdtrilem  11421  bdtri  11422  addcn2  11492  fsumadd  11588  isumadd  11613  binomlem  11665  efaddlem  11856  ef4p  11876  cosval  11885  cosf  11887  tanval2ap  11895  tanval3ap  11896  resin4p  11900  recos4p  11901  efival  11914  sinadd  11918  cosadd  11919  tanaddap  11921  pythagtriplem1  12459  pythagtriplem12  12469  pythagtriplem16  12473  pythagtriplem17  12474  pcbc  12545  mul4sqlem  12587  4sqlem14  12598  oddennn  12634  mulgdirlem  13359  gsumfzconst  13547  gsumfzfsumlemm  14219  addccncf  14920  limcimolemlt  14984  dvaddxxbr  15021  plyaddlem1  15067  ptolemy  15144  rpcxpadd  15225  binom4  15299  lgsquad2lem1  15406  2lgslem3d1  15425  qdencn  15758  iooref1o  15765  apdifflemr  15778