Theorem addcld 11142

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7355  ℂcc 11015   + caddc 11020

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  cnegex  11305  addcom  11310  addcomd  11326  muladd11r  11337  negeu  11361  addsubass  11381  subsub2  11400  subsub4  11405  pnncan  11413  addsub4  11415  addsubsub23  11536  pnpncand  11549  addmulsub  11590  subaddmulsub  11591  mulsubaddmulsub  11592  divdir  11812  cju  12132  cnref1o  12889  xov1plusxeqvd  13405  modaddb  13820  expaddz  14020  binom3  14138  sqoddm1div8  14157  mulsubdivbinom2  14176  muldivbinom2  14177  spllen  14668  crre  15028  remullem  15042  imval2  15065  cjreim2  15075  sqreulem  15274  bhmafibid1cn  15380  bhmafibid2cn  15381  bhmafibid1  15382  bhmafibid2  15383  addcn2  15508  o1add  15528  rlimadd  15557  fsumadd  15654  isumadd  15681  binomlem  15743  binomfallfaclem2  15954  bpoly4  15973  fsumcube  15974  efaddlem  16007  ef4p  16029  cosf  16041  tanval2  16049  tanval3  16050  resin4p  16054  recos4p  16055  efival  16068  sinadd  16080  cosadd  16081  tanadd  16083  pwp1fsum  16309  sadadd2lem2  16368  sadadd2lem  16377  pythagtriplem1  16735  pythagtriplem12  16745  pythagtriplem17  16750  pcbc  16819  mul4sqlem  16872  4sqlem14  16877  vdwlem6  16905  vdwlem9  16908  mulgdirlem  19026  blcvx  24733  cphpyth  25163  tcphcphlem1  25182  cphipval2  25188  4cphipval2  25189  csbren  25346  ovollb2lem  25436  mbfadd  25609  itgcnlem  25738  itgaddlem2  25772  dvmptre  25920  dvsincos  25932  itgpowd  26004  taylthlem2  26329  taylthlem2OLD  26330  ptolemy  26452  tanregt0  26495  eff1olem  26504  cosargd  26564  tanarg  26575  logf1o2  26606  efopn  26614  cxpsqrtlem  26658  cxpeq  26714  ang180lem1  26766  ang180lem2  26767  ang180lem3  26768  ang180lem4  26769  pythag  26774  ssscongptld  26779  chordthmlem  26789  chordthmlem2  26790  chordthmlem3  26791  chordthmlem4  26792  chordthmlem5  26793  heron  26795  quad2  26796  dcubic1lem  26800  dcubic2  26801  dcubic1  26802  dcubic  26803  mcubic  26804  cubic2  26805  cubic  26806  binom4  26807  dquartlem1  26808  dquartlem2  26809  dquart  26810  quart1cl  26811  quart1lem  26812  quart1  26813  quartlem1  26814  quartlem2  26815  quartlem3  26816  quartlem4  26817  quart  26818  asinlem3  26828  asinf  26829  asinneg  26843  efiasin  26845  asinsinlem  26848  asinsin  26849  asinbnd  26856  atanlogaddlem  26870  dmgmaddnn0  26984  dmgmdivn0  26985  lgamgulmlem2  26987  lgamgulmlem3  26988  lgamgulmlem4  26989  lgamgulmlem5  26990  lgamgulmlem6  26991  lgamgulm2  26993  lgambdd  26994  lgamucov  26995  lgamcvg2  27012  gamcvg  27013  gamcvg2lem  27016  ftalem7  27036  basellem3  27040  bposlem9  27250  lgsquad2lem1  27342  2lgslem3d1  27361  2sqmod  27394  dchrvmasumiflem2  27460  mulogsumlem  27489  mulog2sumlem1  27492  mulog2sumlem2  27493  mulog2sumlem3  27494  selberglem1  27503  selberg2  27509  selberg3lem1  27515  selbergr  27526  selberg3r  27527  pntrlog2bndlem1  27535  pntrlog2bndlem2  27536  pntrlog2bndlem5  27539  pntrlog2bndlem6  27541  pntrlog2bnd  27542  brbtwn2  28904  colinearalglem1  28905  colinearalglem2  28906  axeuclidlem  28961  axcontlem2  28964  axcontlem7  28969  axcontlem8  28970  finsumvtxdg2ssteplem4  29548  wwlksext2clwwlk  30058  4ipval2  30709  dipcj  30715  golem1  32272  submuladdd  32747  binom2subadd  32749  pythagreim  32753  quad3d  32757  lt2addrd  32758  cycpmco2lem3  33138  cycpmco2lem4  33139  cycpmco2lem5  33140  cycpmco2lem6  33141  cycpmco2  33143  archirngz  33199  archiabllem2c  33205  zringfrac  33563  ccfldextdgrr  33757  constrrtll  33816  constrrtlc1  33817  constrrtcclem  33819  constrrtcc  33820  constrfin  33831  nn0constr  33846  constraddcl  33847  constrrecl  33854  constrresqrtcl  33862  constrsqrtcl  33864  cos9thpiminplylem1  33867  cos9thpiminplylem2  33868  cos9thpiminplylem3  33869  cos9thpiminply  33873  cos9thpinconstrlem1  33874  cos9thpinconstrlem2  33875  cnre2csqima  33996  ballotlemsima  34601  hgt750lemb  34741  iprodgam  35858  dnizphlfeqhlf  36592  dnibndlem9  36602  knoppndvlem16  36643  itg2addnclem3  37786  itgaddnclem2  37792  itgaddnc  37793  ftc1anclem6  37811  ftc1anclem8  37813  dvasin  37817  areacirclem1  37821  areacirclem4  37824  areacirc  37826  lcmineqlem6  42200  lcmineqlem11  42205  lcmineqlem18  42212  aks4d1p1p2  42236  aks4d1p1p6  42239  aks4d1p1p7  42240  aks4d1p1p5  42241  posbezout  42266  2np3bcnp1  42310  2ap1caineq  42311  sticksstones12a  42323  bcle2d  42345  mvrrsubd  42444  lsubrotld  42447  oddnumth  42481  sumcubes  42483  cxp112d  42511  cxp111d  42512  sn-negex12  42587  sn-addrid  42591  sn-subeu  42597  sn-0tie0  42621  zaddcomlem  42633  zaddcom  42634  cnreeu  42660  dffltz  42792  cu3addd  42838  3cubeslem2  42842  3cubeslem3l  42843  3cubeslem3r  42844  3cubeslem4  42846  pellexlem2  42987  pellexlem6  42991  pell1234qrreccl  43011  pell1234qrmulcl  43012  pell14qrdich  43026  rmxyneg  43077  rmxyadd  43078  jm2.19lem4  43149  jm2.26lem3  43158  sqrtcval  43798  int-rightdistd  44337  binomcxplemnn0  44506  binomcxplemrat  44507  binomcxplemfrat  44508  binomcxplemdvbinom  44510  binomcxplemnotnn0  44513  sub2times  45437  clim1fr1  45763  limcperiod  45790  addlimc  45808  coseq0  46024  fprodaddrecnncnvlem  46069  dvxpaek  46100  dvnxpaek  46102  dvnmul  46103  itgiccshift  46140  itgperiod  46141  stoweidlem1  46161  stoweidlem11  46171  stoweidlem13  46173  wallispilem4  46228  wallispilem5  46229  wallispi  46230  wallispi2lem1  46231  wallispi2lem2  46232  wallispi2  46233  stirlinglem1  46234  stirlinglem3  46236  stirlinglem4  46237  stirlinglem5  46238  stirlinglem6  46239  stirlinglem7  46240  stirlinglem10  46243  stirlinglem11  46244  stirlinglem12  46245  stirlinglem13  46246  stirlinglem15  46248  dirkerper  46256  dirkertrigeqlem1  46258  dirkertrigeqlem2  46259  dirkertrigeqlem3  46260  dirkeritg  46262  dirkercncflem2  46264  dirkercncflem4  46266  fourierdlem18  46285  fourierdlem26  46293  fourierdlem30  46297  fourierdlem48  46314  fourierdlem49  46315  fourierdlem79  46345  fourierdlem83  46349  fourierdlem92  46358  fourierdlem93  46359  fourierdlem103  46369  fourierdlem104  46370  fourierdlem111  46377  fourierdlem112  46378  smfmullem1  46951  sigaraf  47013  sigaras  47015  readdcnnred  47465  fldivmod  47500  fmtnorec4  47711  quad1  47782  requad01  47783  requad2  47785  gpgedgvtx1  48224  dignn0flhalflem1  48777  affinecomb2  48865  eenglngeehlnmlem1  48899  itschlc0yqe  48922  itsclc0yqsollem1  48924  itsclc0yqsol  48926  itscnhlc0xyqsol  48927  itsclc0xyqsolr  48931  2itscplem3  48942  itscnhlinecirc02plem1  48944  inlinecirc02plem  48948  sinhpcosh  49901