Theorem addcld 8039

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

Syntax hints:   → wi 4   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   + caddc 7875

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

This theorem is referenced by:  muladd11r  8175  negeu  8210  addsubass  8229  subsub2  8247  subsub4  8252  pnpcan  8258  pnncan  8260  addsub4  8262  pnpncand  8394  apreim  8622  addext  8629  aprcl  8665  aptap  8669  divdirap  8716  recp1lt1  8918  cju  8980  cnref1o  9716  modsumfzodifsn  10467  expaddzap  10654  binom2  10722  binom3  10728  sqoddm1div8  10764  mulsubdivbinom2ap  10782  nn0opthlem1d  10791  reval  10993  imval  10994  crre  11001  remullem  11015  imval2  11038  cjreim2  11048  cnrecnv  11054  resqrexlemcalc1  11158  maxabslemab  11350  maxltsup  11362  max0addsup  11363  minabs  11379  bdtrilem  11382  bdtri  11383  addcn2  11453  fsumadd  11549  isumadd  11574  binomlem  11626  efaddlem  11817  ef4p  11837  cosval  11846  cosf  11848  tanval2ap  11856  tanval3ap  11857  resin4p  11861  recos4p  11862  efival  11875  sinadd  11879  cosadd  11880  tanaddap  11882  pythagtriplem1  12403  pythagtriplem12  12413  pythagtriplem16  12417  pythagtriplem17  12418  pcbc  12489  mul4sqlem  12531  4sqlem14  12542  oddennn  12549  mulgdirlem  13223  gsumfzconst  13411  gsumfzfsumlemm  14075  addccncf  14754  limcimolemlt  14818  dvaddxxbr  14850  plyaddlem1  14893  ptolemy  14959  rpcxpadd  15040  binom4  15111  qdencn  15517  iooref1o  15524  apdifflemr  15537