Theorem addcld 10513

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

Syntax hints:   → wi 4   ∈ wcel 2083  (class class class)co 7023  ℂcc 10388   + caddc 10393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 10450

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  cnegex  10674  addcom  10679  addcomd  10695  muladd11r  10706  negeu  10729  addsubass  10750  subsub2  10768  subsub4  10773  pnncan  10781  addsub4  10783  pnpncand  10915  addmulsub  10956  subaddmulsub  10957  mulsubaddmulsub  10958  divdir  11177  cju  11488  cnref1o  12238  xov1plusxeqvd  12738  expaddz  13327  binom3  13439  sqoddm1div8  13458  mulsubdivbinom2  13476  muldivbinom2  13477  spllen  13956  crre  14311  remullem  14325  imval2  14348  cjreim2  14358  sqreulem  14557  bhmafibid1cn  14661  bhmafibid2cn  14662  bhmafibid1  14663  bhmafibid2  14664  addcn2  14788  o1add  14808  fsumadd  14933  isumadd  14959  binomlem  15021  binomfallfaclem2  15231  bpoly4  15250  fsumcube  15251  efaddlem  15283  ef4p  15303  cosf  15315  tanval2  15323  tanval3  15324  resin4p  15328  recos4p  15329  efival  15342  sinadd  15354  cosadd  15355  tanadd  15357  pwp1fsum  15579  sadadd2lem2  15636  sadadd2lem  15645  pythagtriplem1  15986  pythagtriplem12  15996  pythagtriplem17  16001  pcbc  16069  mul4sqlem  16122  4sqlem14  16127  vdwlem6  16155  vdwlem9  16158  mulgdirlem  18016  blcvx  23093  tcphcphlem1  23525  cphipval2  23531  4cphipval2  23532  csbren  23689  ovollb2lem  23776  mbfadd  23949  itgcnlem  24077  itgaddlem2  24111  dvmptre  24253  dvsincos  24265  taylthlem2  24649  ptolemy  24769  tanregt0  24808  eff1olem  24817  cosargd  24876  tanarg  24887  logf1o2  24918  efopn  24926  cxpsqrtlem  24970  cxpeq  25023  ang180lem1  25072  ang180lem2  25073  ang180lem3  25074  ang180lem4  25075  pythag  25080  ssscongptld  25085  chordthmlem  25095  chordthmlem2  25096  chordthmlem3  25097  chordthmlem4  25098  chordthmlem5  25099  heron  25101  quad2  25102  dcubic1lem  25106  dcubic2  25107  dcubic1  25108  dcubic  25109  mcubic  25110  cubic2  25111  cubic  25112  binom4  25113  dquartlem1  25114  dquartlem2  25115  dquart  25116  quart1cl  25117  quart1lem  25118  quart1  25119  quartlem1  25120  quartlem2  25121  quartlem3  25122  quartlem4  25123  quart  25124  asinlem3  25134  asinf  25135  asinneg  25149  efiasin  25151  asinsinlem  25154  asinsin  25155  asinbnd  25162  atanlogaddlem  25176  dmgmaddnn0  25290  dmgmdivn0  25291  lgamgulmlem2  25293  lgamgulmlem3  25294  lgamgulmlem4  25295  lgamgulmlem5  25296  lgamgulmlem6  25297  lgamgulm2  25299  lgambdd  25300  lgamucov  25301  lgamcvg2  25318  gamcvg  25319  gamcvg2lem  25322  ftalem7  25342  basellem3  25346  bposlem9  25554  lgsquad2lem1  25646  2lgslem3d1  25665  2sqmod  25698  dchrvmasumiflem2  25764  mulogsumlem  25793  mulog2sumlem1  25796  mulog2sumlem2  25797  mulog2sumlem3  25798  selberglem1  25807  selberg2  25813  selberg3lem1  25819  selbergr  25830  selberg3r  25831  pntrlog2bndlem1  25839  pntrlog2bndlem2  25840  pntrlog2bndlem5  25843  pntrlog2bndlem6  25845  pntrlog2bnd  25846  brbtwn2  26378  colinearalglem1  26379  colinearalglem2  26380  axeuclidlem  26435  axcontlem2  26438  axcontlem7  26443  axcontlem8  26444  finsumvtxdg2ssteplem4  27017  wwlksext2clwwlk  27522  4ipval2  28172  dipcj  28178  golem1  29735  lt2addrd  30159  archirngz  30452  archiabllem2c  30458  ccfldextdgrr  30657  cnre2csqima  30767  ballotlemsima  31386  hgt750lemb  31540  iprodgam  32584  dnizphlfeqhlf  33426  dnibndlem9  33436  knoppndvlem16  33477  itg2addnclem3  34497  itgaddnclem2  34503  itgaddnc  34504  ftc1anclem6  34524  ftc1anclem8  34526  dvasin  34530  areacirclem1  34534  areacirclem4  34537  areacirc  34539  dffltz  38789  pellexlem2  38933  pellexlem6  38937  pell1234qrreccl  38957  pell1234qrmulcl  38958  pell14qrdich  38972  rmxyneg  39023  rmxyadd  39024  jm2.19lem4  39095  jm2.26lem3  39104  itgpowd  39327  int-rightdistd  40040  binomcxplemnn0  40240  binomcxplemrat  40241  binomcxplemfrat  40242  binomcxplemdvbinom  40244  binomcxplemnotnn0  40247  sub2times  41102  clim1fr1  41445  limcperiod  41472  addlimc  41492  coseq0  41708  fprodaddrecnncnvlem  41756  dvxpaek  41788  dvnxpaek  41790  dvnmul  41791  itgiccshift  41828  itgperiod  41829  stoweidlem1  41850  stoweidlem11  41860  stoweidlem13  41862  wallispilem4  41917  wallispilem5  41918  wallispi  41919  wallispi2lem1  41920  wallispi2lem2  41921  wallispi2  41922  stirlinglem1  41923  stirlinglem3  41925  stirlinglem4  41926  stirlinglem5  41927  stirlinglem6  41928  stirlinglem7  41929  stirlinglem10  41932  stirlinglem11  41933  stirlinglem12  41934  stirlinglem13  41935  stirlinglem15  41937  dirkerper  41945  dirkertrigeqlem1  41947  dirkertrigeqlem2  41948  dirkertrigeqlem3  41949  dirkeritg  41951  dirkercncflem2  41953  dirkercncflem4  41955  fourierdlem18  41974  fourierdlem26  41982  fourierdlem30  41986  fourierdlem48  42003  fourierdlem49  42004  fourierdlem79  42034  fourierdlem83  42038  fourierdlem92  42047  fourierdlem93  42048  fourierdlem103  42058  fourierdlem104  42059  fourierdlem111  42066  fourierdlem112  42067  smfmullem1  42630  sigaraf  42674  sigaras  42676  readdcnnred  43041  fmtnorec4  43215  quad1  43289  requad01  43290  requad2  43292  fldivmod  44081  dignn0flhalflem1  44178  affinecomb2  44193  eenglngeehlnmlem1  44227  itschlc0yqe  44250  itsclc0yqsollem1  44252  itsclc0yqsol  44254  itscnhlc0xyqsol  44255  itsclc0xyqsolr  44259  2itscplem3  44270  itscnhlinecirc02plem1  44272  inlinecirc02plem  44276  sinhpcosh  44341