Theorem addcld 8112

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

Syntax hints:   → wi 4   ∈ wcel 2177  (class class class)co 5957  ℂcc 7943   + caddc 7948

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

This theorem is referenced by:  muladd11r  8248  negeu  8283  addsubass  8302  subsub2  8320  subsub4  8325  pnpcan  8331  pnncan  8333  addsub4  8335  pnpncand  8467  apreim  8696  addext  8703  aprcl  8739  aptap  8743  divdirap  8790  recp1lt1  8992  cju  9054  cnref1o  9792  modsumfzodifsn  10563  expaddzap  10750  binom2  10818  binom3  10824  sqoddm1div8  10860  mulsubdivbinom2ap  10878  nn0opthlem1d  10887  reval  11235  imval  11236  crre  11243  remullem  11257  imval2  11280  cjreim2  11290  cnrecnv  11296  resqrexlemcalc1  11400  maxabslemab  11592  maxltsup  11604  max0addsup  11605  minabs  11622  bdtrilem  11625  bdtri  11626  addcn2  11696  fsumadd  11792  isumadd  11817  binomlem  11869  efaddlem  12060  ef4p  12080  cosval  12089  cosf  12091  tanval2ap  12099  tanval3ap  12100  resin4p  12104  recos4p  12105  efival  12118  sinadd  12122  cosadd  12123  tanaddap  12125  pythagtriplem1  12663  pythagtriplem12  12673  pythagtriplem16  12677  pythagtriplem17  12678  pcbc  12749  mul4sqlem  12791  4sqlem14  12802  oddennn  12838  mulgdirlem  13564  gsumfzconst  13752  gsumfzfsumlemm  14424  addccncf  15147  limcimolemlt  15211  dvaddxxbr  15248  plyaddlem1  15294  ptolemy  15371  rpcxpadd  15452  binom4  15526  lgsquad2lem1  15633  2lgslem3d1  15652  qdencn  16107  iooref1o  16114  apdifflemr  16127