Theorem addcld 11367

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237   + caddc 11242

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

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

This theorem is used by:  cnegex  11530  addcom  11535  addcomd  11551  muladd11r  11562  negeu  11586  addsubass  11606  subsub2  11625  subsub4  11630  pnncan  11638  addsub4  11640  addsubsub23  11761  mvrrsubd  11768  pnpncand  11776  addmulsub  11818  subaddmulsub  11819  mulsubaddmulsub  11820  divdir  12039  cju  12356  cnref1o  13153  xov1plusxeqvd  13669  modaddb  14089  expaddz  14289  addmuldir2d  14396  binom3  14409  sqoddm1div8  14428  mulsubdivbinom2  14447  muldivbinom2  14448  spllen  14945  crre  15324  remullem  15338  imval2  15361  cjreim2  15371  sqreulem  15571  bhmafibid1cn  15677  bhmafibid2cn  15678  bhmafibid1  15679  bhmafibid2  15680  addcn2  15805  o1add  15825  rlimadd  15854  fsumadd  15950  isumadd  15977  binomlem  16042  binomfallfaclem2  16250  bpoly4  16269  fsumcube  16270  efaddlem  16303  ef4p  16325  cosf  16337  tanval2  16345  tanval3  16346  resin4p  16350  recos4p  16351  efival  16364  sinadd  16376  cosadd  16377  tanadd  16379  pwp1fsum  16605  sadadd2lem2  16664  sadadd2lem  16673  pythagtriplem1  17038  pythagtriplem12  17048  pythagtriplem17  17053  pcbc  17122  mul4sqlem  17175  4sqlem14  17180  vdwlem6  17208  vdwlem9  17211  mulgdirlem  19365  blcvx  25172  cphpyth  25592  tcphcphlem1  25611  cphipval2  25617  4cphipval2  25618  csbren  25775  ovollb2lem  25864  mbfadd  26037  itgcnlem  26165  itgaddlem2  26199  dvmptre  26344  dvsincos  26356  itgpowd  26425  taylthlem2  26758  ptolemy  26882  tanregt0  26924  eff1olem  26933  cosargd  26993  tanarg  27004  logf1o2  27035  efopn  27043  cxpsqrtlem  27087  cxpeq  27142  ang180lem1  27194  ang180lem2  27195  ang180lem3  27196  ang180lem4  27197  pythag  27202  ssscongptld  27207  chordthmlem  27217  chordthmlem2  27218  chordthmlem3  27219  chordthmlem4  27220  chordthmlem5  27221  heron  27223  quad2  27224  dcubic1lem  27228  dcubic2  27229  dcubic1  27230  dcubic  27231  mcubic  27232  cubic2  27233  cubic  27234  binom4  27235  dquartlem1  27236  dquartlem2  27237  dquart  27238  quart1cl  27239  quart1lem  27240  quart1  27241  quartlem1  27242  quartlem2  27243  quartlem3  27244  quartlem4  27245  quart  27246  asinlem3  27256  asinf  27257  asinneg  27271  efiasin  27273  asinsinlem  27276  asinsin  27277  asinbnd  27284  atanlogaddlem  27298  dmgmaddnn0  27411  dmgmdivn0  27412  lgamgulmlem2  27414  lgamgulmlem3  27415  lgamgulmlem4  27416  lgamgulmlem5  27417  lgamgulmlem6  27418  lgamgulm2  27420  lgambdd  27421  lgamucov  27422  lgamcvg2  27439  gamcvg  27440  gamcvg2lem  27443  ftalem7  27463  basellem3  27467  bposlem9  27676  lgsquad2lem1  27768  2lgslem3d1  27787  2sqmod  27820  dchrvmasumiflem2  27886  mulogsumlem  27915  mulog2sumlem1  27918  mulog2sumlem2  27919  mulog2sumlem3  27920  selberglem1  27929  selberg2  27935  selberg3lem1  27941  selbergr  27952  selberg3r  27953  pntrlog2bndlem1  27961  pntrlog2bndlem2  27962  pntrlog2bndlem5  27965  pntrlog2bndlem6  27967  pntrlog2bnd  27968  brbtwn2  29540  colinearalglem1  29541  colinearalglem2  29542  axeuclidlem  29597  axcontlem2  29600  axcontlem7  29605  axcontlem8  29606  finsumvtxdg2ssteplem4  30186  wwlksext2clwwlk  30705  4ipval2  31367  dipcj  31373  golem1  32930  submuladdd  33428  binom2subadd  33429  pythagreim  33433  quad3d  33437  lt2addrd  33438  cycpmco2lem3  33788  cycpmco2lem4  33789  cycpmco2lem5  33790  cycpmco2lem6  33791  cycpmco2  33793  archirngz  33849  archiabllem2c  33855  zringfrac  34189  ccfldextdgrr  34415  constrrtll  34474  constrrtlc1  34475  constrrtcclem  34477  constrrtcc  34478  constrfin  34489  nn0constr  34504  constraddcl  34505  constrrecl  34512  constrresqrtcl  34520  constrsqrtcl  34522  cos9thpiminplylem1  34525  cos9thpiminplylem2  34526  cos9thpiminplylem3  34527  cos9thpiminply  34531  cos9thpinconstrlem1  34532  cos9thpinconstrlem2  34533  cnre2csqima  34654  ballotlemsima  35259  hgt750lemb  35396  iprodgam  36722  dnizphlfeqhlf  37557  dnibndlem9  37567  knoppndvlem16  37608  qdiff  38516  itg2addnclem3  38859  itgaddnclem2  38865  itgaddnc  38866  ftc1anclem6  38884  ftc1anclem8  38886  dvasin  38890  areacirclem1  38894  areacirclem4  38897  areacirc  38899  lcmineqlem6  43350  lcmineqlem11  43355  lcmineqlem18  43362  aks4d1p1p2  43386  aks4d1p1p6  43389  aks4d1p1p7  43390  aks4d1p1p5  43391  posbezout  43416  2np3bcnp1  43460  2ap1caineq  43461  sticksstones12a  43473  bcle2d  43495  quadfac  43521  lsubrotld  43600  oddnumth  43634  sumcubes  43636  cxp112d  43658  cxp111d  43659  sn-negex12  43734  sn-addrid  43738  sn-subeu  43744  sn-0tie0  43781  zaddcomlem  43793  zaddcom  43794  cnreeu  43820  dffltz  43936  cu3addd  43957  3cubeslem2  43961  3cubeslem3l  43962  3cubeslem3r  43963  3cubeslem4  43965  pellexlem2  44103  pellexlem6  44107  pell1234qrreccl  44127  pell1234qrmulcl  44128  pell14qrdich  44142  rmxyneg  44193  rmxyadd  44194  jm2.19lem4  44265  jm2.26lem3  44274  sqrtcval  44902  int-rightdistd  45441  binomcxplemnn0  45594  binomcxplemrat  45595  binomcxplemfrat  45596  binomcxplemdvbinom  45598  binomcxplemnotnn0  45601  sub2times  46562  clim1fr1  46886  limcperiod  46913  addlimc  46931  coseq0  47147  fprodaddrecnncnvlem  47192  dvxpaek  47223  dvnxpaek  47225  dvnmul  47226  itgiccshift  47263  itgperiod  47264  stoweidlem1  47284  stoweidlem11  47294  stoweidlem13  47296  wallispilem4  47351  wallispilem5  47352  wallispi  47353  wallispi2lem1  47354  wallispi2lem2  47355  wallispi2  47356  stirlinglem1  47357  stirlinglem3  47359  stirlinglem4  47360  stirlinglem5  47361  stirlinglem6  47362  stirlinglem7  47363  stirlinglem10  47366  stirlinglem11  47367  stirlinglem12  47368  stirlinglem13  47369  stirlinglem15  47371  dirkerper  47379  dirkertrigeqlem1  47381  dirkertrigeqlem2  47382  dirkertrigeqlem3  47383  dirkeritg  47385  dirkercncflem2  47387  dirkercncflem4  47389  fourierdlem18  47408  fourierdlem26  47416  fourierdlem30  47420  fourierdlem48  47437  fourierdlem49  47438  fourierdlem79  47468  fourierdlem83  47472  fourierdlem92  47481  fourierdlem93  47482  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  fourierdlem112  47501  smfmullem1  48074  sigaraf  48136  sigaras  48138  sin5tlem1  48192  sin5tlem4  48195  sin5tlem5  48196  readdcnnred  48646  fldivmod  48687  fmtnorec4  48907  quad1  48991  requad01  48992  requad2  48994  gpgedgvtx1  49433  lazlinz  49733  dignn0flhalflem1  50058  affinecomb2  50146  eenglngeehlnmlem1  50181  itschlc0yqe  50203  itsclc0yqsollem1  50205  itsclc0yqsol  50207  itscnhlc0xyqsol  50208  itsclc0xyqsolr  50212  2itscplem3  50223  itscnhlinecirc02plem1  50225  inlinecirc02plem  50229  sinhpcosh  51238  tanhadd  51258  crossp3d  51395  veroquadgsumlem  51411