Theorem addcld 8174

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

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

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

This theorem is referenced by:  muladd11r  8310  negeu  8345  addsubass  8364  subsub2  8382  subsub4  8387  pnpcan  8393  pnncan  8395  addsub4  8397  pnpncand  8529  apreim  8758  addext  8765  aprcl  8801  aptap  8805  divdirap  8852  recp1lt1  9054  cju  9116  cnref1o  9854  modsumfzodifsn  10626  expaddzap  10813  binom2  10881  binom3  10887  sqoddm1div8  10923  mulsubdivbinom2ap  10941  nn0opthlem1d  10950  reval  11368  imval  11369  crre  11376  remullem  11390  imval2  11413  cjreim2  11423  cnrecnv  11429  resqrexlemcalc1  11533  maxabslemab  11725  maxltsup  11737  max0addsup  11738  minabs  11755  bdtrilem  11758  bdtri  11759  addcn2  11829  fsumadd  11925  isumadd  11950  binomlem  12002  efaddlem  12193  ef4p  12213  cosval  12222  cosf  12224  tanval2ap  12232  tanval3ap  12233  resin4p  12237  recos4p  12238  efival  12251  sinadd  12255  cosadd  12256  tanaddap  12258  pythagtriplem1  12796  pythagtriplem12  12806  pythagtriplem16  12810  pythagtriplem17  12811  pcbc  12882  mul4sqlem  12924  4sqlem14  12935  oddennn  12971  mulgdirlem  13698  gsumfzconst  13886  gsumfzfsumlemm  14559  addccncf  15282  limcimolemlt  15346  dvaddxxbr  15383  plyaddlem1  15429  ptolemy  15506  rpcxpadd  15587  binom4  15661  lgsquad2lem1  15768  2lgslem3d1  15787  qdencn  16422  iooref1o  16429  apdifflemr  16442