Theorem addcld 7570

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

Syntax hints:   → wi 4   ∈ wcel 1439  (class class class)co 5668  ℂcc 7411   + caddc 7416

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

This theorem is referenced by:  muladd11r  7701  negeu  7736  addsubass  7755  subsub2  7773  subsub4  7778  pnpcan  7784  pnncan  7786  addsub4  7788  pnpncand  7916  apreim  8143  addext  8150  divdirap  8227  recp1lt1  8423  cju  8484  cnref1o  9196  modsumfzodifsn  9866  ser3add  9998  expaddzap  10062  binom2  10128  binom3  10134  sqoddm1div8  10169  nn0opthlem1d  10191  reval  10346  imval  10347  crre  10354  remullem  10368  imval2  10391  cjreim2  10401  cnrecnv  10407  resqrexlemcalc1  10510  maxabslemab  10702  maxltsup  10714  max0addsup  10715  addcn2  10762  fsumadd  10863  isumadd  10888  binomlem  10940  efaddlem  11027  ef4p  11047  cosval  11057  cosf  11059  tanval2ap  11067  tanval3ap  11068  resin4p  11072  recos4p  11073  efival  11086  sinadd  11090  cosadd  11091  tanaddap  11093  oddennn  11546  qdencn  12218