Theorem addcld 8335

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

Syntax hints:   → wi 4   ∈ wcel 2209  (class class class)co 6075  ℂcc 8167   + caddc 8172

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

This theorem is referenced by:  muladd11r  8472  negeu  8507  addsubass  8526  subsub2  8544  subsub4  8549  pnpcan  8555  pnncan  8557  addsub4  8559  pnpncand  8691  apreim  8921  addext  8928  aprcl  8964  aptap  8968  divdirap  9017  recp1lt1  9219  cju  9281  cnref1o  10030  modsumfzodifsn  10811  expaddzap  10998  binom2  11066  binom3  11072  sqoddm1div8  11109  mulsubdivbinom2ap  11127  nn0opthlem1d  11136  reval  11592  imval  11593  crre  11600  remullem  11614  imval2  11637  cjreim2  11648  cnrecnv  11654  resqrexlemcalc1  11758  maxabslemab  11950  maxltsup  11962  max0addsup  11963  minabs  11980  bdtrilem  11983  bdtri  11984  addcn2  12054  fsumadd  12151  isumadd  12176  binomlem  12228  efaddlem  12419  ef4p  12439  cosval  12448  cosf  12450  tanval2ap  12458  tanval3ap  12459  resin4p  12463  recos4p  12464  efival  12477  sinadd  12481  cosadd  12482  tanaddap  12484  pythagtriplem1  13022  pythagtriplem12  13032  pythagtriplem16  13036  pythagtriplem17  13037  pcbc  13108  mul4sqlem  13150  4sqlem14  13161  ballotfilemsima  13237  oddennn  13261  mulgdirlem  13933  gzsumconst  14120  gsumfsum  14895  addccncf  15624  limcimolemlt  15688  dvaddxxbr  15725  plyaddlem1  15771  ptolemy  15848  rpcxpadd  15930  binom4  16004  pellexlem2  16006  lgsquad2lem1  16114  2lgslem3d1  16133  dichmul0orlem7  16673  qdencn  16977  iooref1o  16988  apdifflemr  17001  qdiff  17003