Theorem addcld 11280

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   + caddc 11158

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

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

This theorem is referenced by:  cnegex  11442  addcom  11447  addcomd  11463  muladd11r  11474  negeu  11498  addsubass  11518  subsub2  11537  subsub4  11542  pnncan  11550  addsub4  11552  pnpncand  11684  addmulsub  11725  subaddmulsub  11726  mulsubaddmulsub  11727  divdir  11947  cju  12262  cnref1o  13027  xov1plusxeqvd  13538  expaddz  14147  binom3  14263  sqoddm1div8  14282  mulsubdivbinom2  14301  muldivbinom2  14302  spllen  14792  crre  15153  remullem  15167  imval2  15190  cjreim2  15200  sqreulem  15398  bhmafibid1cn  15502  bhmafibid2cn  15503  bhmafibid1  15504  bhmafibid2  15505  addcn2  15630  o1add  15650  rlimadd  15679  fsumadd  15776  isumadd  15803  binomlem  15865  binomfallfaclem2  16076  bpoly4  16095  fsumcube  16096  efaddlem  16129  ef4p  16149  cosf  16161  tanval2  16169  tanval3  16170  resin4p  16174  recos4p  16175  efival  16188  sinadd  16200  cosadd  16201  tanadd  16203  pwp1fsum  16428  sadadd2lem2  16487  sadadd2lem  16496  pythagtriplem1  16854  pythagtriplem12  16864  pythagtriplem17  16869  pcbc  16938  mul4sqlem  16991  4sqlem14  16996  vdwlem6  17024  vdwlem9  17027  mulgdirlem  19123  blcvx  24819  cphpyth  25250  tcphcphlem1  25269  cphipval2  25275  4cphipval2  25276  csbren  25433  ovollb2lem  25523  mbfadd  25696  itgcnlem  25825  itgaddlem2  25859  dvmptre  26007  dvsincos  26019  itgpowd  26091  taylthlem2  26416  taylthlem2OLD  26417  ptolemy  26538  tanregt0  26581  eff1olem  26590  cosargd  26650  tanarg  26661  logf1o2  26692  efopn  26700  cxpsqrtlem  26744  cxpeq  26800  ang180lem1  26852  ang180lem2  26853  ang180lem3  26854  ang180lem4  26855  pythag  26860  ssscongptld  26865  chordthmlem  26875  chordthmlem2  26876  chordthmlem3  26877  chordthmlem4  26878  chordthmlem5  26879  heron  26881  quad2  26882  dcubic1lem  26886  dcubic2  26887  dcubic1  26888  dcubic  26889  mcubic  26890  cubic2  26891  cubic  26892  binom4  26893  dquartlem1  26894  dquartlem2  26895  dquart  26896  quart1cl  26897  quart1lem  26898  quart1  26899  quartlem1  26900  quartlem2  26901  quartlem3  26902  quartlem4  26903  quart  26904  asinlem3  26914  asinf  26915  asinneg  26929  efiasin  26931  asinsinlem  26934  asinsin  26935  asinbnd  26942  atanlogaddlem  26956  dmgmaddnn0  27070  dmgmdivn0  27071  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamgulm2  27079  lgambdd  27080  lgamucov  27081  lgamcvg2  27098  gamcvg  27099  gamcvg2lem  27102  ftalem7  27122  basellem3  27126  bposlem9  27336  lgsquad2lem1  27428  2lgslem3d1  27447  2sqmod  27480  dchrvmasumiflem2  27546  mulogsumlem  27575  mulog2sumlem1  27578  mulog2sumlem2  27579  mulog2sumlem3  27580  selberglem1  27589  selberg2  27595  selberg3lem1  27601  selbergr  27612  selberg3r  27613  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  brbtwn2  28920  colinearalglem1  28921  colinearalglem2  28922  axeuclidlem  28977  axcontlem2  28980  axcontlem7  28985  axcontlem8  28986  finsumvtxdg2ssteplem4  29566  wwlksext2clwwlk  30076  4ipval2  30727  dipcj  30733  golem1  32290  submuladdd  32750  quad3d  32754  lt2addrd  32755  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2  33153  archirngz  33196  archiabllem2c  33202  zringfrac  33582  ccfldextdgrr  33722  constrrtll  33772  constrrtlc1  33773  constrrtcclem  33775  constrrtcc  33776  constrfin  33787  cnre2csqima  33910  ballotlemsima  34518  hgt750lemb  34671  iprodgam  35742  dnizphlfeqhlf  36477  dnibndlem9  36487  knoppndvlem16  36528  itg2addnclem3  37680  itgaddnclem2  37686  itgaddnc  37687  ftc1anclem6  37705  ftc1anclem8  37707  dvasin  37711  areacirclem1  37715  areacirclem4  37718  areacirc  37720  lcmineqlem6  42035  lcmineqlem11  42040  lcmineqlem18  42047  aks4d1p1p2  42071  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  posbezout  42101  2np3bcnp1  42145  2ap1caineq  42146  sticksstones12a  42158  bcle2d  42180  metakunt29  42234  mvrrsubd  42309  lsubrotld  42312  oddnumth  42345  sumcubes  42347  cxp112d  42377  cxp111d  42378  sn-negex12  42446  sn-addrid  42450  sn-subeu  42456  sn-0tie0  42469  zaddcomlem  42481  zaddcom  42482  cnreeu  42500  dffltz  42644  cu3addd  42691  3cubeslem2  42696  3cubeslem3l  42697  3cubeslem3r  42698  3cubeslem4  42700  pellexlem2  42841  pellexlem6  42845  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell14qrdich  42880  rmxyneg  42932  rmxyadd  42933  jm2.19lem4  43004  jm2.26lem3  43013  sqrtcval  43654  int-rightdistd  44193  binomcxplemnn0  44368  binomcxplemrat  44369  binomcxplemfrat  44370  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  sub2times  45284  clim1fr1  45616  limcperiod  45643  addlimc  45663  coseq0  45879  fprodaddrecnncnvlem  45924  dvxpaek  45955  dvnxpaek  45957  dvnmul  45958  itgiccshift  45995  itgperiod  45996  stoweidlem1  46016  stoweidlem11  46026  stoweidlem13  46028  wallispilem4  46083  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem1  46089  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlinglem15  46103  dirkerper  46111  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkeritg  46117  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem18  46140  fourierdlem26  46148  fourierdlem30  46152  fourierdlem48  46169  fourierdlem49  46170  fourierdlem79  46200  fourierdlem83  46204  fourierdlem92  46213  fourierdlem93  46214  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  smfmullem1  46806  sigaraf  46868  sigaras  46870  readdcnnred  47315  fldivmod  47340  fmtnorec4  47536  quad1  47607  requad01  47608  requad2  47610  gpgedgvtx1  48020  dignn0flhalflem1  48536  affinecomb2  48624  eenglngeehlnmlem1  48658  itschlc0yqe  48681  itsclc0yqsollem1  48683  itsclc0yqsol  48685  itscnhlc0xyqsol  48686  itsclc0xyqsolr  48690  2itscplem3  48701  itscnhlinecirc02plem1  48703  inlinecirc02plem  48707  sinhpcosh  49259