Theorem addcld 11155

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   + caddc 11032

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

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

This theorem is referenced by:  cnegex  11318  addcom  11323  addcomd  11339  muladd11r  11350  negeu  11374  addsubass  11394  subsub2  11413  subsub4  11418  pnncan  11426  addsub4  11428  addsubsub23  11549  pnpncand  11562  addmulsub  11603  subaddmulsub  11604  mulsubaddmulsub  11605  divdir  11825  cju  12146  cnref1o  12926  xov1plusxeqvd  13442  modaddb  13859  expaddz  14059  binom3  14177  sqoddm1div8  14196  mulsubdivbinom2  14215  muldivbinom2  14216  spllen  14707  crre  15067  remullem  15081  imval2  15104  cjreim2  15114  sqreulem  15313  bhmafibid1cn  15419  bhmafibid2cn  15420  bhmafibid1  15421  bhmafibid2  15422  addcn2  15547  o1add  15567  rlimadd  15596  fsumadd  15693  isumadd  15720  binomlem  15785  binomfallfaclem2  15996  bpoly4  16015  fsumcube  16016  efaddlem  16049  ef4p  16071  cosf  16083  tanval2  16091  tanval3  16092  resin4p  16096  recos4p  16097  efival  16110  sinadd  16122  cosadd  16123  tanadd  16125  pwp1fsum  16351  sadadd2lem2  16410  sadadd2lem  16419  pythagtriplem1  16778  pythagtriplem12  16788  pythagtriplem17  16793  pcbc  16862  mul4sqlem  16915  4sqlem14  16920  vdwlem6  16948  vdwlem9  16951  mulgdirlem  19072  blcvx  24773  cphpyth  25193  tcphcphlem1  25212  cphipval2  25218  4cphipval2  25219  csbren  25376  ovollb2lem  25465  mbfadd  25638  itgcnlem  25767  itgaddlem2  25801  dvmptre  25946  dvsincos  25958  itgpowd  26027  taylthlem2  26351  taylthlem2OLD  26352  ptolemy  26473  tanregt0  26516  eff1olem  26525  cosargd  26585  tanarg  26596  logf1o2  26627  efopn  26635  cxpsqrtlem  26679  cxpeq  26734  ang180lem1  26786  ang180lem2  26787  ang180lem3  26788  ang180lem4  26789  pythag  26794  ssscongptld  26799  chordthmlem  26809  chordthmlem2  26810  chordthmlem3  26811  chordthmlem4  26812  chordthmlem5  26813  heron  26815  quad2  26816  dcubic1lem  26820  dcubic2  26821  dcubic1  26822  dcubic  26823  mcubic  26824  cubic2  26825  cubic  26826  binom4  26827  dquartlem1  26828  dquartlem2  26829  dquart  26830  quart1cl  26831  quart1lem  26832  quart1  26833  quartlem1  26834  quartlem2  26835  quartlem3  26836  quartlem4  26837  quart  26838  asinlem3  26848  asinf  26849  asinneg  26863  efiasin  26865  asinsinlem  26868  asinsin  26869  asinbnd  26876  atanlogaddlem  26890  dmgmaddnn0  27004  dmgmdivn0  27005  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem4  27009  lgamgulmlem5  27010  lgamgulmlem6  27011  lgamgulm2  27013  lgambdd  27014  lgamucov  27015  lgamcvg2  27032  gamcvg  27033  gamcvg2lem  27036  ftalem7  27056  basellem3  27060  bposlem9  27269  lgsquad2lem1  27361  2lgslem3d1  27380  2sqmod  27413  dchrvmasumiflem2  27479  mulogsumlem  27508  mulog2sumlem1  27511  mulog2sumlem2  27512  mulog2sumlem3  27513  selberglem1  27522  selberg2  27528  selberg3lem1  27534  selbergr  27545  selberg3r  27546  pntrlog2bndlem1  27554  pntrlog2bndlem2  27555  pntrlog2bndlem5  27558  pntrlog2bndlem6  27560  pntrlog2bnd  27561  brbtwn2  28988  colinearalglem1  28989  colinearalglem2  28990  axeuclidlem  29045  axcontlem2  29048  axcontlem7  29053  axcontlem8  29054  finsumvtxdg2ssteplem4  29632  wwlksext2clwwlk  30142  4ipval2  30794  dipcj  30800  golem1  32357  submuladdd  32828  binom2subadd  32829  pythagreim  32833  quad3d  32837  lt2addrd  32838  cycpmco2lem3  33204  cycpmco2lem4  33205  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2  33209  archirngz  33265  archiabllem2c  33271  zringfrac  33629  ccfldextdgrr  33832  constrrtll  33891  constrrtlc1  33892  constrrtcclem  33894  constrrtcc  33895  constrfin  33906  nn0constr  33921  constraddcl  33922  constrrecl  33929  constrresqrtcl  33937  constrsqrtcl  33939  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  cos9thpiminplylem3  33944  cos9thpiminply  33948  cos9thpinconstrlem1  33949  cos9thpinconstrlem2  33950  cnre2csqima  34071  ballotlemsima  34676  hgt750lemb  34816  iprodgam  35940  dnizphlfeqhlf  36752  dnibndlem9  36762  knoppndvlem16  36803  itg2addnclem3  38008  itgaddnclem2  38014  itgaddnc  38015  ftc1anclem6  38033  ftc1anclem8  38035  dvasin  38039  areacirclem1  38043  areacirclem4  38046  areacirc  38048  lcmineqlem6  42487  lcmineqlem11  42492  lcmineqlem18  42499  aks4d1p1p2  42523  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  posbezout  42553  2np3bcnp1  42597  2ap1caineq  42598  sticksstones12a  42610  bcle2d  42632  mvrrsubd  42720  lsubrotld  42723  oddnumth  42757  sumcubes  42759  cxp112d  42787  cxp111d  42788  sn-negex12  42863  sn-addrid  42867  sn-subeu  42873  sn-0tie0  42910  zaddcomlem  42922  zaddcom  42923  cnreeu  42949  dffltz  43081  cu3addd  43127  3cubeslem2  43131  3cubeslem3l  43132  3cubeslem3r  43133  3cubeslem4  43135  pellexlem2  43276  pellexlem6  43280  pell1234qrreccl  43300  pell1234qrmulcl  43301  pell14qrdich  43315  rmxyneg  43366  rmxyadd  43367  jm2.19lem4  43438  jm2.26lem3  43447  sqrtcval  44086  int-rightdistd  44625  binomcxplemnn0  44794  binomcxplemrat  44795  binomcxplemfrat  44796  binomcxplemdvbinom  44798  binomcxplemnotnn0  44801  sub2times  45724  clim1fr1  46049  limcperiod  46076  addlimc  46094  coseq0  46310  fprodaddrecnncnvlem  46355  dvxpaek  46386  dvnxpaek  46388  dvnmul  46389  itgiccshift  46426  itgperiod  46427  stoweidlem1  46447  stoweidlem11  46457  stoweidlem13  46459  wallispilem4  46514  wallispilem5  46515  wallispi  46516  wallispi2lem1  46517  wallispi2lem2  46518  wallispi2  46519  stirlinglem1  46520  stirlinglem3  46522  stirlinglem4  46523  stirlinglem5  46524  stirlinglem6  46525  stirlinglem7  46526  stirlinglem10  46529  stirlinglem11  46530  stirlinglem12  46531  stirlinglem13  46532  stirlinglem15  46534  dirkerper  46542  dirkertrigeqlem1  46544  dirkertrigeqlem2  46545  dirkertrigeqlem3  46546  dirkeritg  46548  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem18  46571  fourierdlem26  46579  fourierdlem30  46583  fourierdlem48  46600  fourierdlem49  46601  fourierdlem79  46631  fourierdlem83  46635  fourierdlem92  46644  fourierdlem93  46645  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  smfmullem1  47237  sigaraf  47299  sigaras  47301  sin5tlem1  47337  sin5tlem4  47340  sin5tlem5  47341  readdcnnred  47763  fldivmod  47804  fmtnorec4  48024  quad1  48108  requad01  48109  requad2  48111  gpgedgvtx1  48550  dignn0flhalflem1  49103  affinecomb2  49191  eenglngeehlnmlem1  49225  itschlc0yqe  49248  itsclc0yqsollem1  49250  itsclc0yqsol  49252  itscnhlc0xyqsol  49253  itsclc0xyqsolr  49257  2itscplem3  49268  itscnhlinecirc02plem1  49270  inlinecirc02plem  49274  sinhpcosh  50227