Theorem addcld 8041

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

Syntax hints:   → wi 4   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   + caddc 7877

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

This theorem is referenced by:  muladd11r  8177  negeu  8212  addsubass  8231  subsub2  8249  subsub4  8254  pnpcan  8260  pnncan  8262  addsub4  8264  pnpncand  8396  apreim  8624  addext  8631  aprcl  8667  aptap  8671  divdirap  8718  recp1lt1  8920  cju  8982  cnref1o  9719  modsumfzodifsn  10470  expaddzap  10657  binom2  10725  binom3  10731  sqoddm1div8  10767  mulsubdivbinom2ap  10785  nn0opthlem1d  10794  reval  10996  imval  10997  crre  11004  remullem  11018  imval2  11041  cjreim2  11051  cnrecnv  11057  resqrexlemcalc1  11161  maxabslemab  11353  maxltsup  11365  max0addsup  11366  minabs  11382  bdtrilem  11385  bdtri  11386  addcn2  11456  fsumadd  11552  isumadd  11577  binomlem  11629  efaddlem  11820  ef4p  11840  cosval  11849  cosf  11851  tanval2ap  11859  tanval3ap  11860  resin4p  11864  recos4p  11865  efival  11878  sinadd  11882  cosadd  11883  tanaddap  11885  pythagtriplem1  12406  pythagtriplem12  12416  pythagtriplem16  12420  pythagtriplem17  12421  pcbc  12492  mul4sqlem  12534  4sqlem14  12545  oddennn  12552  mulgdirlem  13226  gsumfzconst  13414  gsumfzfsumlemm  14086  addccncf  14779  limcimolemlt  14843  dvaddxxbr  14880  plyaddlem1  14926  ptolemy  15000  rpcxpadd  15081  binom4  15152  lgsquad2lem1  15238  2lgslem3d1  15257  qdencn  15587  iooref1o  15594  apdifflemr  15607