Theorem addcld 11223

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

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   + caddc 11098

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  cnegex  11386  addcom  11391  addcomd  11407  muladd11r  11418  negeu  11442  addsubass  11462  subsub2  11481  subsub4  11486  pnncan  11494  addsub4  11496  addsubsub23  11617  pnpncand  11630  addmulsub  11671  subaddmulsub  11672  mulsubaddmulsub  11673  divdir  11892  cju  12209  cnref1o  13004  xov1plusxeqvd  13520  modaddb  13938  expaddz  14138  binom3  14256  sqoddm1div8  14275  mulsubdivbinom2  14294  muldivbinom2  14295  spllen  14787  crre  15161  remullem  15175  imval2  15198  cjreim2  15208  sqreulem  15407  bhmafibid1cn  15513  bhmafibid2cn  15514  bhmafibid1  15515  bhmafibid2  15516  addcn2  15641  o1add  15661  rlimadd  15690  fsumadd  15787  isumadd  15814  binomlem  15879  binomfallfaclem2  16089  bpoly4  16108  fsumcube  16109  efaddlem  16142  ef4p  16164  cosf  16176  tanval2  16184  tanval3  16185  resin4p  16189  recos4p  16190  efival  16203  sinadd  16215  cosadd  16216  tanadd  16218  pwp1fsum  16444  sadadd2lem2  16503  sadadd2lem  16512  pythagtriplem1  16871  pythagtriplem12  16881  pythagtriplem17  16886  pcbc  16955  mul4sqlem  17008  4sqlem14  17013  vdwlem6  17041  vdwlem9  17044  mulgdirlem  19166  blcvx  24955  cphpyth  25375  tcphcphlem1  25394  cphipval2  25400  4cphipval2  25401  csbren  25558  ovollb2lem  25647  mbfadd  25820  itgcnlem  25949  itgaddlem2  25983  dvmptre  26128  dvsincos  26140  itgpowd  26209  taylthlem2  26537  ptolemy  26661  tanregt0  26704  eff1olem  26713  cosargd  26773  tanarg  26784  logf1o2  26815  efopn  26823  cxpsqrtlem  26867  cxpeq  26922  ang180lem1  26974  ang180lem2  26975  ang180lem3  26976  ang180lem4  26977  pythag  26982  ssscongptld  26987  chordthmlem  26997  chordthmlem2  26998  chordthmlem3  26999  chordthmlem4  27000  chordthmlem5  27001  heron  27003  quad2  27004  dcubic1lem  27008  dcubic2  27009  dcubic1  27010  dcubic  27011  mcubic  27012  cubic2  27013  cubic  27014  binom4  27015  dquartlem1  27016  dquartlem2  27017  dquart  27018  quart1cl  27019  quart1lem  27020  quart1  27021  quartlem1  27022  quartlem2  27023  quartlem3  27024  quartlem4  27025  quart  27026  asinlem3  27036  asinf  27037  asinneg  27051  efiasin  27053  asinsinlem  27056  asinsin  27057  asinbnd  27064  atanlogaddlem  27078  dmgmaddnn0  27191  dmgmdivn0  27192  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem4  27196  lgamgulmlem5  27197  lgamgulmlem6  27198  lgamgulm2  27200  lgambdd  27201  lgamucov  27202  lgamcvg2  27219  gamcvg  27220  gamcvg2lem  27223  ftalem7  27243  basellem3  27247  bposlem9  27456  lgsquad2lem1  27548  2lgslem3d1  27567  2sqmod  27600  dchrvmasumiflem2  27666  mulogsumlem  27695  mulog2sumlem1  27698  mulog2sumlem2  27699  mulog2sumlem3  27700  selberglem1  27709  selberg2  27715  selberg3lem1  27721  selbergr  27732  selberg3r  27733  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntrlog2bnd  27748  brbtwn2  29255  colinearalglem1  29256  colinearalglem2  29257  axeuclidlem  29312  axcontlem2  29315  axcontlem7  29320  axcontlem8  29321  finsumvtxdg2ssteplem4  29898  wwlksext2clwwlk  30408  4ipval2  31060  dipcj  31066  golem1  32623  submuladdd  33085  binom2subadd  33086  pythagreim  33090  quad3d  33094  lt2addrd  33095  cycpmco2lem3  33448  cycpmco2lem4  33449  cycpmco2lem5  33450  cycpmco2lem6  33451  cycpmco2  33453  archirngz  33509  archiabllem2c  33515  zringfrac  33844  ccfldextdgrr  34062  constrrtll  34121  constrrtlc1  34122  constrrtcclem  34124  constrrtcc  34125  constrfin  34136  nn0constr  34151  constraddcl  34152  constrrecl  34159  constrresqrtcl  34167  constrsqrtcl  34169  cos9thpiminplylem1  34172  cos9thpiminplylem2  34173  cos9thpiminplylem3  34174  cos9thpiminply  34178  cos9thpinconstrlem1  34179  cos9thpinconstrlem2  34180  cnre2csqima  34301  ballotlemsima  34906  hgt750lemb  35043  iprodgam  36234  dnizphlfeqhlf  37065  dnibndlem9  37075  knoppndvlem16  37116  qdiff  37971  itg2addnclem3  38324  itgaddnclem2  38330  itgaddnc  38331  ftc1anclem6  38349  ftc1anclem8  38351  dvasin  38355  areacirclem1  38359  areacirclem4  38362  areacirc  38364  lcmineqlem6  42801  lcmineqlem11  42806  lcmineqlem18  42813  aks4d1p1p2  42837  aks4d1p1p6  42840  aks4d1p1p7  42841  aks4d1p1p5  42842  posbezout  42867  2np3bcnp1  42911  2ap1caineq  42912  sticksstones12a  42924  bcle2d  42946  quadfac  42972  mvrrsubd  43035  lsubrotld  43038  oddnumth  43072  sumcubes  43074  cxp112d  43102  cxp111d  43103  sn-negex12  43178  sn-addrid  43182  sn-subeu  43188  sn-0tie0  43225  zaddcomlem  43237  zaddcom  43238  cnreeu  43264  dffltz  43366  cu3addd  43412  3cubeslem2  43416  3cubeslem3l  43417  3cubeslem3r  43418  3cubeslem4  43420  pellexlem2  43557  pellexlem6  43561  pell1234qrreccl  43581  pell1234qrmulcl  43582  pell14qrdich  43596  rmxyneg  43647  rmxyadd  43648  jm2.19lem4  43719  jm2.26lem3  43728  sqrtcval  44367  int-rightdistd  44906  binomcxplemnn0  45059  binomcxplemrat  45060  binomcxplemfrat  45061  binomcxplemdvbinom  45063  binomcxplemnotnn0  45066  sub2times  45992  clim1fr1  46317  limcperiod  46344  addlimc  46362  coseq0  46578  fprodaddrecnncnvlem  46623  dvxpaek  46654  dvnxpaek  46656  dvnmul  46657  itgiccshift  46694  itgperiod  46695  stoweidlem1  46715  stoweidlem11  46725  stoweidlem13  46727  wallispilem4  46782  wallispilem5  46783  wallispi  46784  wallispi2lem1  46785  wallispi2lem2  46786  wallispi2  46787  stirlinglem1  46788  stirlinglem3  46790  stirlinglem4  46791  stirlinglem5  46792  stirlinglem6  46793  stirlinglem7  46794  stirlinglem10  46797  stirlinglem11  46798  stirlinglem12  46799  stirlinglem13  46800  stirlinglem15  46802  dirkerper  46810  dirkertrigeqlem1  46812  dirkertrigeqlem2  46813  dirkertrigeqlem3  46814  dirkeritg  46816  dirkercncflem2  46818  dirkercncflem4  46820  fourierdlem18  46839  fourierdlem26  46847  fourierdlem30  46851  fourierdlem48  46868  fourierdlem49  46869  fourierdlem79  46899  fourierdlem83  46903  fourierdlem92  46912  fourierdlem93  46913  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  fourierdlem112  46932  smfmullem1  47505  sigaraf  47567  sigaras  47569  sin5tlem1  47610  sin5tlem4  47613  sin5tlem5  47614  readdcnnred  48040  fldivmod  48081  fmtnorec4  48301  quad1  48385  requad01  48386  requad2  48388  gpgedgvtx1  48827  dignn0flhalflem1  49395  affinecomb2  49483  eenglngeehlnmlem1  49517  itschlc0yqe  49540  itsclc0yqsollem1  49542  itsclc0yqsol  49544  itscnhlc0xyqsol  49545  itsclc0xyqsolr  49549  2itscplem3  49560  itscnhlinecirc02plem1  49562  inlinecirc02plem  49566  sinhpcosh  50518