Theorem addcld 8198

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6017  ℂcc 8029   + caddc 8034

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

This theorem is referenced by:  muladd11r  8334  negeu  8369  addsubass  8388  subsub2  8406  subsub4  8411  pnpcan  8417  pnncan  8419  addsub4  8421  pnpncand  8553  apreim  8782  addext  8789  aprcl  8825  aptap  8829  divdirap  8876  recp1lt1  9078  cju  9140  cnref1o  9884  modsumfzodifsn  10657  expaddzap  10844  binom2  10912  binom3  10918  sqoddm1div8  10954  mulsubdivbinom2ap  10972  nn0opthlem1d  10981  reval  11409  imval  11410  crre  11417  remullem  11431  imval2  11454  cjreim2  11464  cnrecnv  11470  resqrexlemcalc1  11574  maxabslemab  11766  maxltsup  11778  max0addsup  11779  minabs  11796  bdtrilem  11799  bdtri  11800  addcn2  11870  fsumadd  11966  isumadd  11991  binomlem  12043  efaddlem  12234  ef4p  12254  cosval  12263  cosf  12265  tanval2ap  12273  tanval3ap  12274  resin4p  12278  recos4p  12279  efival  12292  sinadd  12296  cosadd  12297  tanaddap  12299  pythagtriplem1  12837  pythagtriplem12  12847  pythagtriplem16  12851  pythagtriplem17  12852  pcbc  12923  mul4sqlem  12965  4sqlem14  12976  oddennn  13012  mulgdirlem  13739  gsumfzconst  13927  gsumfzfsumlemm  14600  addccncf  15323  limcimolemlt  15387  dvaddxxbr  15424  plyaddlem1  15470  ptolemy  15547  rpcxpadd  15628  binom4  15702  lgsquad2lem1  15809  2lgslem3d1  15828  qdencn  16631  iooref1o  16638  apdifflemr  16651