Theorem addcld 8293

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

Syntax hints:   → wi 4   ∈ wcel 2203  (class class class)co 6050  ℂcc 8125   + caddc 8130

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

This theorem is referenced by:  muladd11r  8429  negeu  8464  addsubass  8483  subsub2  8501  subsub4  8506  pnpcan  8512  pnncan  8514  addsub4  8516  pnpncand  8648  apreim  8877  addext  8884  aprcl  8920  aptap  8924  divdirap  8971  recp1lt1  9173  cju  9235  cnref1o  9983  modsumfzodifsn  10758  expaddzap  10945  binom2  11013  binom3  11019  sqoddm1div8  11055  mulsubdivbinom2ap  11073  nn0opthlem1d  11082  reval  11534  imval  11535  crre  11542  remullem  11556  imval2  11579  cjreim2  11589  cnrecnv  11595  resqrexlemcalc1  11699  maxabslemab  11891  maxltsup  11903  max0addsup  11904  minabs  11921  bdtrilem  11924  bdtri  11925  addcn2  11995  fsumadd  12092  isumadd  12117  binomlem  12169  efaddlem  12360  ef4p  12380  cosval  12389  cosf  12391  tanval2ap  12399  tanval3ap  12400  resin4p  12404  recos4p  12405  efival  12418  sinadd  12422  cosadd  12423  tanaddap  12425  pythagtriplem1  12963  pythagtriplem12  12973  pythagtriplem16  12977  pythagtriplem17  12978  pcbc  13049  mul4sqlem  13091  4sqlem14  13102  oddennn  13143  mulgdirlem  13870  gsumfzconst  14058  gsumfzfsumlemm  14735  addccncf  15465  limcimolemlt  15529  dvaddxxbr  15566  plyaddlem1  15612  ptolemy  15689  rpcxpadd  15770  binom4  15844  pellexlem2  15846  lgsquad2lem1  15954  2lgslem3d1  15973  qdencn  16807  iooref1o  16818  apdifflemr  16831  qdiff  16833