Theorem addcld 11333

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7422  ℂcc 11203   + caddc 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 11265

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  cnegex  11496  addcom  11501  addcomd  11517  muladd11r  11528  negeu  11552  addsubass  11572  subsub2  11591  subsub4  11596  pnncan  11604  addsub4  11606  addsubsub23  11727  mvrrsubd  11734  pnpncand  11742  addmulsub  11783  subaddmulsub  11784  mulsubaddmulsub  11785  divdir  12004  cju  12321  cnref1o  13118  xov1plusxeqvd  13634  modaddb  14054  expaddz  14254  binom3  14373  sqoddm1div8  14392  mulsubdivbinom2  14411  muldivbinom2  14412  spllen  14909  crre  15288  remullem  15302  imval2  15325  cjreim2  15335  sqreulem  15534  bhmafibid1cn  15640  bhmafibid2cn  15641  bhmafibid1  15642  bhmafibid2  15643  addcn2  15768  o1add  15788  rlimadd  15817  fsumadd  15913  isumadd  15940  binomlem  16005  binomfallfaclem2  16213  bpoly4  16232  fsumcube  16233  efaddlem  16266  ef4p  16288  cosf  16300  tanval2  16308  tanval3  16309  resin4p  16313  recos4p  16314  efival  16327  sinadd  16339  cosadd  16340  tanadd  16342  pwp1fsum  16568  sadadd2lem2  16627  sadadd2lem  16636  pythagtriplem1  17001  pythagtriplem12  17011  pythagtriplem17  17016  pcbc  17085  mul4sqlem  17138  4sqlem14  17143  vdwlem6  17171  vdwlem9  17174  mulgdirlem  19322  blcvx  25124  cphpyth  25544  tcphcphlem1  25563  cphipval2  25569  4cphipval2  25570  csbren  25727  ovollb2lem  25816  mbfadd  25989  itgcnlem  26117  itgaddlem2  26151  dvmptre  26296  dvsincos  26308  itgpowd  26377  taylthlem2  26708  ptolemy  26832  tanregt0  26874  eff1olem  26883  cosargd  26943  tanarg  26954  logf1o2  26985  efopn  26993  cxpsqrtlem  27037  cxpeq  27092  ang180lem1  27144  ang180lem2  27145  ang180lem3  27146  ang180lem4  27147  pythag  27152  ssscongptld  27157  chordthmlem  27167  chordthmlem2  27168  chordthmlem3  27169  chordthmlem4  27170  chordthmlem5  27171  heron  27173  quad2  27174  dcubic1lem  27178  dcubic2  27179  dcubic1  27180  dcubic  27181  mcubic  27182  cubic2  27183  cubic  27184  binom4  27185  dquartlem1  27186  dquartlem2  27187  dquart  27188  quart1cl  27189  quart1lem  27190  quart1  27191  quartlem1  27192  quartlem2  27193  quartlem3  27194  quartlem4  27195  quart  27196  asinlem3  27206  asinf  27207  asinneg  27221  efiasin  27223  asinsinlem  27226  asinsin  27227  asinbnd  27234  atanlogaddlem  27248  dmgmaddnn0  27361  dmgmdivn0  27362  lgamgulmlem2  27364  lgamgulmlem3  27365  lgamgulmlem4  27366  lgamgulmlem5  27367  lgamgulmlem6  27368  lgamgulm2  27370  lgambdd  27371  lgamucov  27372  lgamcvg2  27389  gamcvg  27390  gamcvg2lem  27393  ftalem7  27413  basellem3  27417  bposlem9  27626  lgsquad2lem1  27718  2lgslem3d1  27737  2sqmod  27770  dchrvmasumiflem2  27836  mulogsumlem  27865  mulog2sumlem1  27868  mulog2sumlem2  27869  mulog2sumlem3  27870  selberglem1  27879  selberg2  27885  selberg3lem1  27891  selbergr  27902  selberg3r  27903  pntrlog2bndlem1  27911  pntrlog2bndlem2  27912  pntrlog2bndlem5  27915  pntrlog2bndlem6  27917  pntrlog2bnd  27918  brbtwn2  29490  colinearalglem1  29491  colinearalglem2  29492  axeuclidlem  29547  axcontlem2  29550  axcontlem7  29555  axcontlem8  29556  finsumvtxdg2ssteplem4  30136  wwlksext2clwwlk  30655  4ipval2  31317  dipcj  31323  golem1  32880  submuladdd  33380  binom2subadd  33381  pythagreim  33385  quad3d  33389  lt2addrd  33390  cycpmco2lem3  33737  cycpmco2lem4  33738  cycpmco2lem5  33739  cycpmco2lem6  33740  cycpmco2  33742  archirngz  33798  archiabllem2c  33804  zringfrac  34134  ccfldextdgrr  34352  constrrtll  34411  constrrtlc1  34412  constrrtcclem  34414  constrrtcc  34415  constrfin  34426  nn0constr  34441  constraddcl  34442  constrrecl  34449  constrresqrtcl  34457  constrsqrtcl  34459  cos9thpiminplylem1  34462  cos9thpiminplylem2  34463  cos9thpiminplylem3  34464  cos9thpiminply  34468  cos9thpinconstrlem1  34469  cos9thpinconstrlem2  34470  cnre2csqima  34591  ballotlemsima  35196  hgt750lemb  35333  iprodgam  36601  dnizphlfeqhlf  37436  dnibndlem9  37446  knoppndvlem16  37487  qdiff  38355  itg2addnclem3  38698  itgaddnclem2  38704  itgaddnc  38705  ftc1anclem6  38723  ftc1anclem8  38725  dvasin  38729  areacirclem1  38733  areacirclem4  38736  areacirc  38738  lcmineqlem6  43191  lcmineqlem11  43196  lcmineqlem18  43203  aks4d1p1p2  43227  aks4d1p1p6  43230  aks4d1p1p7  43231  aks4d1p1p5  43232  posbezout  43257  2np3bcnp1  43301  2ap1caineq  43302  sticksstones12a  43314  bcle2d  43336  quadfac  43362  lsubrotld  43441  oddnumth  43475  sumcubes  43477  cxp112d  43499  cxp111d  43500  sn-negex12  43575  sn-addrid  43579  sn-subeu  43585  sn-0tie0  43622  zaddcomlem  43634  zaddcom  43635  cnreeu  43661  dffltz  43777  cu3addd  43798  3cubeslem2  43802  3cubeslem3l  43803  3cubeslem3r  43804  3cubeslem4  43806  pellexlem2  43944  pellexlem6  43948  pell1234qrreccl  43968  pell1234qrmulcl  43969  pell14qrdich  43983  rmxyneg  44034  rmxyadd  44035  jm2.19lem4  44106  jm2.26lem3  44115  sqrtcval  44748  int-rightdistd  45287  binomcxplemnn0  45440  binomcxplemrat  45441  binomcxplemfrat  45442  binomcxplemdvbinom  45444  binomcxplemnotnn0  45447  sub2times  46396  clim1fr1  46720  limcperiod  46747  addlimc  46765  coseq0  46981  fprodaddrecnncnvlem  47026  dvxpaek  47057  dvnxpaek  47059  dvnmul  47060  itgiccshift  47097  itgperiod  47098  stoweidlem1  47118  stoweidlem11  47128  stoweidlem13  47130  wallispilem4  47185  wallispilem5  47186  wallispi  47187  wallispi2lem1  47188  wallispi2lem2  47189  wallispi2  47190  stirlinglem1  47191  stirlinglem3  47193  stirlinglem4  47194  stirlinglem5  47195  stirlinglem6  47196  stirlinglem7  47197  stirlinglem10  47200  stirlinglem11  47201  stirlinglem12  47202  stirlinglem13  47203  stirlinglem15  47205  dirkerper  47213  dirkertrigeqlem1  47215  dirkertrigeqlem2  47216  dirkertrigeqlem3  47217  dirkeritg  47219  dirkercncflem2  47221  dirkercncflem4  47223  fourierdlem18  47242  fourierdlem26  47250  fourierdlem30  47254  fourierdlem48  47271  fourierdlem49  47272  fourierdlem79  47302  fourierdlem83  47306  fourierdlem92  47315  fourierdlem93  47316  fourierdlem103  47326  fourierdlem104  47327  fourierdlem111  47334  fourierdlem112  47335  smfmullem1  47908  sigaraf  47970  sigaras  47972  sin5tlem1  48026  sin5tlem4  48029  sin5tlem5  48030  readdcnnred  48480  fldivmod  48521  fmtnorec4  48741  quad1  48825  requad01  48826  requad2  48828  gpgedgvtx1  49267  dignn0flhalflem1  49834  affinecomb2  49922  eenglngeehlnmlem1  49957  itschlc0yqe  49979  itsclc0yqsollem1  49981  itsclc0yqsol  49983  itscnhlc0xyqsol  49984  itsclc0xyqsolr  49988  2itscplem3  49999  itscnhlinecirc02plem1  50001  inlinecirc02plem  50005  sinhpcosh  51015  crossp3d  51149  veroquadgsumlem  51165