Theorem addcld 8177

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6007  ℂcc 8008   + caddc 8013

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

This theorem is referenced by:  muladd11r  8313  negeu  8348  addsubass  8367  subsub2  8385  subsub4  8390  pnpcan  8396  pnncan  8398  addsub4  8400  pnpncand  8532  apreim  8761  addext  8768  aprcl  8804  aptap  8808  divdirap  8855  recp1lt1  9057  cju  9119  cnref1o  9858  modsumfzodifsn  10630  expaddzap  10817  binom2  10885  binom3  10891  sqoddm1div8  10927  mulsubdivbinom2ap  10945  nn0opthlem1d  10954  reval  11375  imval  11376  crre  11383  remullem  11397  imval2  11420  cjreim2  11430  cnrecnv  11436  resqrexlemcalc1  11540  maxabslemab  11732  maxltsup  11744  max0addsup  11745  minabs  11762  bdtrilem  11765  bdtri  11766  addcn2  11836  fsumadd  11932  isumadd  11957  binomlem  12009  efaddlem  12200  ef4p  12220  cosval  12229  cosf  12231  tanval2ap  12239  tanval3ap  12240  resin4p  12244  recos4p  12245  efival  12258  sinadd  12262  cosadd  12263  tanaddap  12265  pythagtriplem1  12803  pythagtriplem12  12813  pythagtriplem16  12817  pythagtriplem17  12818  pcbc  12889  mul4sqlem  12931  4sqlem14  12942  oddennn  12978  mulgdirlem  13705  gsumfzconst  13893  gsumfzfsumlemm  14566  addccncf  15289  limcimolemlt  15353  dvaddxxbr  15390  plyaddlem1  15436  ptolemy  15513  rpcxpadd  15594  binom4  15668  lgsquad2lem1  15775  2lgslem3d1  15794  qdencn  16455  iooref1o  16462  apdifflemr  16475