Theorem addcld 8046

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

Syntax hints:   → wi 4   ∈ wcel 2167  (class class class)co 5922  ℂcc 7877   + caddc 7882

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

This theorem is referenced by:  muladd11r  8182  negeu  8217  addsubass  8236  subsub2  8254  subsub4  8259  pnpcan  8265  pnncan  8267  addsub4  8269  pnpncand  8401  apreim  8630  addext  8637  aprcl  8673  aptap  8677  divdirap  8724  recp1lt1  8926  cju  8988  cnref1o  9725  modsumfzodifsn  10488  expaddzap  10675  binom2  10743  binom3  10749  sqoddm1div8  10785  mulsubdivbinom2ap  10803  nn0opthlem1d  10812  reval  11014  imval  11015  crre  11022  remullem  11036  imval2  11059  cjreim2  11069  cnrecnv  11075  resqrexlemcalc1  11179  maxabslemab  11371  maxltsup  11383  max0addsup  11384  minabs  11401  bdtrilem  11404  bdtri  11405  addcn2  11475  fsumadd  11571  isumadd  11596  binomlem  11648  efaddlem  11839  ef4p  11859  cosval  11868  cosf  11870  tanval2ap  11878  tanval3ap  11879  resin4p  11883  recos4p  11884  efival  11897  sinadd  11901  cosadd  11902  tanaddap  11904  pythagtriplem1  12434  pythagtriplem12  12444  pythagtriplem16  12448  pythagtriplem17  12449  pcbc  12520  mul4sqlem  12562  4sqlem14  12573  oddennn  12609  mulgdirlem  13283  gsumfzconst  13471  gsumfzfsumlemm  14143  addccncf  14836  limcimolemlt  14900  dvaddxxbr  14937  plyaddlem1  14983  ptolemy  15060  rpcxpadd  15141  binom4  15215  lgsquad2lem1  15322  2lgslem3d1  15341  qdencn  15671  iooref1o  15678  apdifflemr  15691