Theorem addcld 11224

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

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7408  ℂcc 11094   + caddc 11099

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

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

This theorem is referenced by:  cnegex  11387  addcom  11392  addcomd  11408  muladd11r  11419  negeu  11443  addsubass  11463  subsub2  11482  subsub4  11487  pnncan  11495  addsub4  11497  addsubsub23  11618  pnpncand  11631  addmulsub  11672  subaddmulsub  11673  mulsubaddmulsub  11674  divdir  11893  cju  12210  cnref1o  13005  xov1plusxeqvd  13521  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  16090  bpoly4  16109  fsumcube  16110  efaddlem  16143  ef4p  16165  cosf  16177  tanval2  16185  tanval3  16186  resin4p  16190  recos4p  16191  efival  16204  sinadd  16216  cosadd  16217  tanadd  16219  pwp1fsum  16445  sadadd2lem2  16504  sadadd2lem  16513  pythagtriplem1  16872  pythagtriplem12  16882  pythagtriplem17  16887  pcbc  16956  mul4sqlem  17009  4sqlem14  17014  vdwlem6  17042  vdwlem9  17045  mulgdirlem  19167  blcvx  24920  cphpyth  25340  tcphcphlem1  25359  cphipval2  25365  4cphipval2  25366  csbren  25523  ovollb2lem  25612  mbfadd  25785  itgcnlem  25914  itgaddlem2  25948  dvmptre  26093  dvsincos  26105  itgpowd  26174  taylthlem2  26499  ptolemy  26623  tanregt0  26666  eff1olem  26675  cosargd  26735  tanarg  26746  logf1o2  26777  efopn  26785  cxpsqrtlem  26829  cxpeq  26884  ang180lem1  26936  ang180lem2  26937  ang180lem3  26938  ang180lem4  26939  pythag  26944  ssscongptld  26949  chordthmlem  26959  chordthmlem2  26960  chordthmlem3  26961  chordthmlem4  26962  chordthmlem5  26963  heron  26965  quad2  26966  dcubic1lem  26970  dcubic2  26971  dcubic1  26972  dcubic  26973  mcubic  26974  cubic2  26975  cubic  26976  binom4  26977  dquartlem1  26978  dquartlem2  26979  dquart  26980  quart1cl  26981  quart1lem  26982  quart1  26983  quartlem1  26984  quartlem2  26985  quartlem3  26986  quartlem4  26987  quart  26988  asinlem3  26998  asinf  26999  asinneg  27013  efiasin  27015  asinsinlem  27018  asinsin  27019  asinbnd  27026  atanlogaddlem  27040  dmgmaddnn0  27153  dmgmdivn0  27154  lgamgulmlem2  27156  lgamgulmlem3  27157  lgamgulmlem4  27158  lgamgulmlem5  27159  lgamgulmlem6  27160  lgamgulm2  27162  lgambdd  27163  lgamucov  27164  lgamcvg2  27181  gamcvg  27182  gamcvg2lem  27185  ftalem7  27205  basellem3  27209  bposlem9  27418  lgsquad2lem1  27510  2lgslem3d1  27529  2sqmod  27562  dchrvmasumiflem2  27628  mulogsumlem  27657  mulog2sumlem1  27660  mulog2sumlem2  27661  mulog2sumlem3  27662  selberglem1  27671  selberg2  27677  selberg3lem1  27683  selbergr  27694  selberg3r  27695  pntrlog2bndlem1  27703  pntrlog2bndlem2  27704  pntrlog2bndlem5  27707  pntrlog2bndlem6  27709  pntrlog2bnd  27710  brbtwn2  29192  colinearalglem1  29193  colinearalglem2  29194  axeuclidlem  29249  axcontlem2  29252  axcontlem7  29257  axcontlem8  29258  finsumvtxdg2ssteplem4  29835  wwlksext2clwwlk  30345  4ipval2  30997  dipcj  31003  golem1  32560  submuladdd  33022  binom2subadd  33023  pythagreim  33027  quad3d  33031  lt2addrd  33032  cycpmco2lem3  33385  cycpmco2lem4  33386  cycpmco2lem5  33387  cycpmco2lem6  33388  cycpmco2  33390  archirngz  33446  archiabllem2c  33452  zringfrac  33785  ccfldextdgrr  34003  constrrtll  34062  constrrtlc1  34063  constrrtcclem  34065  constrrtcc  34066  constrfin  34077  nn0constr  34092  constraddcl  34093  constrrecl  34100  constrresqrtcl  34108  constrsqrtcl  34110  cos9thpiminplylem1  34113  cos9thpiminplylem2  34114  cos9thpiminplylem3  34115  cos9thpiminply  34119  cos9thpinconstrlem1  34120  cos9thpinconstrlem2  34121  cnre2csqima  34242  ballotlemsima  34847  hgt750lemb  34984  iprodgam  36129  dnizphlfeqhlf  36950  dnibndlem9  36960  knoppndvlem16  37001  qdiff  37854  itg2addnclem3  38207  itgaddnclem2  38213  itgaddnc  38214  ftc1anclem6  38232  ftc1anclem8  38234  dvasin  38238  areacirclem1  38242  areacirclem4  38245  areacirc  38247  lcmineqlem6  42686  lcmineqlem11  42691  lcmineqlem18  42698  aks4d1p1p2  42722  aks4d1p1p6  42725  aks4d1p1p7  42726  aks4d1p1p5  42727  posbezout  42752  2np3bcnp1  42796  2ap1caineq  42797  sticksstones12a  42809  bcle2d  42831  quadfac  42857  mvrrsubd  42920  lsubrotld  42923  oddnumth  42957  sumcubes  42959  cxp112d  42987  cxp111d  42988  sn-negex12  43063  sn-addrid  43067  sn-subeu  43073  sn-0tie0  43110  zaddcomlem  43122  zaddcom  43123  cnreeu  43149  dffltz  43253  cu3addd  43299  3cubeslem2  43303  3cubeslem3l  43304  3cubeslem3r  43305  3cubeslem4  43307  pellexlem2  43444  pellexlem6  43448  pell1234qrreccl  43468  pell1234qrmulcl  43469  pell14qrdich  43483  rmxyneg  43534  rmxyadd  43535  jm2.19lem4  43606  jm2.26lem3  43615  sqrtcval  44254  int-rightdistd  44793  binomcxplemnn0  44946  binomcxplemrat  44947  binomcxplemfrat  44948  binomcxplemdvbinom  44950  binomcxplemnotnn0  44953  sub2times  45879  clim1fr1  46204  limcperiod  46231  addlimc  46249  coseq0  46465  fprodaddrecnncnvlem  46510  dvxpaek  46541  dvnxpaek  46543  dvnmul  46544  itgiccshift  46581  itgperiod  46582  stoweidlem1  46602  stoweidlem11  46612  stoweidlem13  46614  wallispilem4  46669  wallispilem5  46670  wallispi  46671  wallispi2lem1  46672  wallispi2lem2  46673  wallispi2  46674  stirlinglem1  46675  stirlinglem3  46677  stirlinglem4  46678  stirlinglem5  46679  stirlinglem6  46680  stirlinglem7  46681  stirlinglem10  46684  stirlinglem11  46685  stirlinglem12  46686  stirlinglem13  46687  stirlinglem15  46689  dirkerper  46697  dirkertrigeqlem1  46699  dirkertrigeqlem2  46700  dirkertrigeqlem3  46701  dirkeritg  46703  dirkercncflem2  46705  dirkercncflem4  46707  fourierdlem18  46726  fourierdlem26  46734  fourierdlem30  46738  fourierdlem48  46755  fourierdlem49  46756  fourierdlem79  46786  fourierdlem83  46790  fourierdlem92  46799  fourierdlem93  46800  fourierdlem103  46810  fourierdlem104  46811  fourierdlem111  46818  fourierdlem112  46819  smfmullem1  47392  sigaraf  47454  sigaras  47456  sin5tlem1  47494  sin5tlem4  47497  sin5tlem5  47498  readdcnnred  47924  fldivmod  47965  fmtnorec4  48185  quad1  48269  requad01  48270  requad2  48272  gpgedgvtx1  48711  dignn0flhalflem1  49275  affinecomb2  49363  eenglngeehlnmlem1  49397  itschlc0yqe  49420  itsclc0yqsollem1  49422  itsclc0yqsol  49424  itscnhlc0xyqsol  49425  itsclc0xyqsolr  49429  2itscplem3  49440  itscnhlinecirc02plem1  49442  inlinecirc02plem  49446  sinhpcosh  50398