Theorem addcld 8241

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   + caddc 8078

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

This theorem is referenced by:  muladd11r  8377  negeu  8412  addsubass  8431  subsub2  8449  subsub4  8454  pnpcan  8460  pnncan  8462  addsub4  8464  pnpncand  8596  apreim  8825  addext  8832  aprcl  8868  aptap  8872  divdirap  8919  recp1lt1  9121  cju  9183  cnref1o  9929  modsumfzodifsn  10704  expaddzap  10891  binom2  10959  binom3  10965  sqoddm1div8  11001  mulsubdivbinom2ap  11019  nn0opthlem1d  11028  reval  11472  imval  11473  crre  11480  remullem  11494  imval2  11517  cjreim2  11527  cnrecnv  11533  resqrexlemcalc1  11637  maxabslemab  11829  maxltsup  11841  max0addsup  11842  minabs  11859  bdtrilem  11862  bdtri  11863  addcn2  11933  fsumadd  12030  isumadd  12055  binomlem  12107  efaddlem  12298  ef4p  12318  cosval  12327  cosf  12329  tanval2ap  12337  tanval3ap  12338  resin4p  12342  recos4p  12343  efival  12356  sinadd  12360  cosadd  12361  tanaddap  12363  pythagtriplem1  12901  pythagtriplem12  12911  pythagtriplem16  12915  pythagtriplem17  12916  pcbc  12987  mul4sqlem  13029  4sqlem14  13040  oddennn  13076  mulgdirlem  13803  gsumfzconst  13991  gsumfzfsumlemm  14666  addccncf  15394  limcimolemlt  15458  dvaddxxbr  15495  plyaddlem1  15541  ptolemy  15618  rpcxpadd  15699  binom4  15773  pellexlem2  15775  lgsquad2lem1  15883  2lgslem3d1  15902  qdencn  16738  iooref1o  16749  apdifflemr  16762  qdiff  16764