Theorem addcld 8162

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6000  ℂcc 7993   + caddc 7998

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

This theorem is referenced by:  muladd11r  8298  negeu  8333  addsubass  8352  subsub2  8370  subsub4  8375  pnpcan  8381  pnncan  8383  addsub4  8385  pnpncand  8517  apreim  8746  addext  8753  aprcl  8789  aptap  8793  divdirap  8840  recp1lt1  9042  cju  9104  cnref1o  9842  modsumfzodifsn  10613  expaddzap  10800  binom2  10868  binom3  10874  sqoddm1div8  10910  mulsubdivbinom2ap  10928  nn0opthlem1d  10937  reval  11355  imval  11356  crre  11363  remullem  11377  imval2  11400  cjreim2  11410  cnrecnv  11416  resqrexlemcalc1  11520  maxabslemab  11712  maxltsup  11724  max0addsup  11725  minabs  11742  bdtrilem  11745  bdtri  11746  addcn2  11816  fsumadd  11912  isumadd  11937  binomlem  11989  efaddlem  12180  ef4p  12200  cosval  12209  cosf  12211  tanval2ap  12219  tanval3ap  12220  resin4p  12224  recos4p  12225  efival  12238  sinadd  12242  cosadd  12243  tanaddap  12245  pythagtriplem1  12783  pythagtriplem12  12793  pythagtriplem16  12797  pythagtriplem17  12798  pcbc  12869  mul4sqlem  12911  4sqlem14  12922  oddennn  12958  mulgdirlem  13685  gsumfzconst  13873  gsumfzfsumlemm  14545  addccncf  15268  limcimolemlt  15332  dvaddxxbr  15369  plyaddlem1  15415  ptolemy  15492  rpcxpadd  15573  binom4  15647  lgsquad2lem1  15754  2lgslem3d1  15773  qdencn  16354  iooref1o  16361  apdifflemr  16374