Theorem addcld 11169

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   + caddc 11047

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

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

This theorem is referenced by:  cnegex  11331  addcom  11336  addcomd  11352  muladd11r  11363  negeu  11387  addsubass  11407  subsub2  11426  subsub4  11431  pnncan  11439  addsub4  11441  addsubsub23  11562  pnpncand  11575  addmulsub  11616  subaddmulsub  11617  mulsubaddmulsub  11618  divdir  11838  cju  12158  cnref1o  12920  xov1plusxeqvd  13435  modaddb  13847  expaddz  14047  binom3  14165  sqoddm1div8  14184  mulsubdivbinom2  14203  muldivbinom2  14204  spllen  14695  crre  15056  remullem  15070  imval2  15093  cjreim2  15103  sqreulem  15302  bhmafibid1cn  15408  bhmafibid2cn  15409  bhmafibid1  15410  bhmafibid2  15411  addcn2  15536  o1add  15556  rlimadd  15585  fsumadd  15682  isumadd  15709  binomlem  15771  binomfallfaclem2  15982  bpoly4  16001  fsumcube  16002  efaddlem  16035  ef4p  16057  cosf  16069  tanval2  16077  tanval3  16078  resin4p  16082  recos4p  16083  efival  16096  sinadd  16108  cosadd  16109  tanadd  16111  pwp1fsum  16337  sadadd2lem2  16396  sadadd2lem  16405  pythagtriplem1  16763  pythagtriplem12  16773  pythagtriplem17  16778  pcbc  16847  mul4sqlem  16900  4sqlem14  16905  vdwlem6  16933  vdwlem9  16936  mulgdirlem  19013  blcvx  24662  cphpyth  25092  tcphcphlem1  25111  cphipval2  25117  4cphipval2  25118  csbren  25275  ovollb2lem  25365  mbfadd  25538  itgcnlem  25667  itgaddlem2  25701  dvmptre  25849  dvsincos  25861  itgpowd  25933  taylthlem2  26258  taylthlem2OLD  26259  ptolemy  26381  tanregt0  26424  eff1olem  26433  cosargd  26493  tanarg  26504  logf1o2  26535  efopn  26543  cxpsqrtlem  26587  cxpeq  26643  ang180lem1  26695  ang180lem2  26696  ang180lem3  26697  ang180lem4  26698  pythag  26703  ssscongptld  26708  chordthmlem  26718  chordthmlem2  26719  chordthmlem3  26720  chordthmlem4  26721  chordthmlem5  26722  heron  26724  quad2  26725  dcubic1lem  26729  dcubic2  26730  dcubic1  26731  dcubic  26732  mcubic  26733  cubic2  26734  cubic  26735  binom4  26736  dquartlem1  26737  dquartlem2  26738  dquart  26739  quart1cl  26740  quart1lem  26741  quart1  26742  quartlem1  26743  quartlem2  26744  quartlem3  26745  quartlem4  26746  quart  26747  asinlem3  26757  asinf  26758  asinneg  26772  efiasin  26774  asinsinlem  26777  asinsin  26778  asinbnd  26785  atanlogaddlem  26799  dmgmaddnn0  26913  dmgmdivn0  26914  lgamgulmlem2  26916  lgamgulmlem3  26917  lgamgulmlem4  26918  lgamgulmlem5  26919  lgamgulmlem6  26920  lgamgulm2  26922  lgambdd  26923  lgamucov  26924  lgamcvg2  26941  gamcvg  26942  gamcvg2lem  26945  ftalem7  26965  basellem3  26969  bposlem9  27179  lgsquad2lem1  27271  2lgslem3d1  27290  2sqmod  27323  dchrvmasumiflem2  27389  mulogsumlem  27418  mulog2sumlem1  27421  mulog2sumlem2  27422  mulog2sumlem3  27423  selberglem1  27432  selberg2  27438  selberg3lem1  27444  selbergr  27455  selberg3r  27456  pntrlog2bndlem1  27464  pntrlog2bndlem2  27465  pntrlog2bndlem5  27468  pntrlog2bndlem6  27470  pntrlog2bnd  27471  brbtwn2  28808  colinearalglem1  28809  colinearalglem2  28810  axeuclidlem  28865  axcontlem2  28868  axcontlem7  28873  axcontlem8  28874  finsumvtxdg2ssteplem4  29452  wwlksext2clwwlk  29959  4ipval2  30610  dipcj  30616  golem1  32173  submuladdd  32636  binom2subadd  32638  pythagreim  32642  quad3d  32646  lt2addrd  32647  cycpmco2lem3  33058  cycpmco2lem4  33059  cycpmco2lem5  33060  cycpmco2lem6  33061  cycpmco2  33063  archirngz  33116  archiabllem2c  33122  zringfrac  33498  ccfldextdgrr  33640  constrrtll  33694  constrrtlc1  33695  constrrtcclem  33697  constrrtcc  33698  constrfin  33709  nn0constr  33724  constraddcl  33725  constrrecl  33732  constrresqrtcl  33740  constrsqrtcl  33742  cos9thpiminplylem1  33745  cos9thpiminplylem2  33746  cos9thpiminplylem3  33747  cos9thpiminply  33751  cos9thpinconstrlem1  33752  cos9thpinconstrlem2  33753  cnre2csqima  33874  ballotlemsima  34480  hgt750lemb  34620  iprodgam  35702  dnizphlfeqhlf  36437  dnibndlem9  36447  knoppndvlem16  36488  itg2addnclem3  37640  itgaddnclem2  37646  itgaddnc  37647  ftc1anclem6  37665  ftc1anclem8  37667  dvasin  37671  areacirclem1  37675  areacirclem4  37678  areacirc  37680  lcmineqlem6  41995  lcmineqlem11  42000  lcmineqlem18  42007  aks4d1p1p2  42031  aks4d1p1p6  42034  aks4d1p1p7  42035  aks4d1p1p5  42036  posbezout  42061  2np3bcnp1  42105  2ap1caineq  42106  sticksstones12a  42118  bcle2d  42140  mvrrsubd  42235  lsubrotld  42238  oddnumth  42272  sumcubes  42274  cxp112d  42302  cxp111d  42303  sn-negex12  42378  sn-addrid  42382  sn-subeu  42388  sn-0tie0  42412  zaddcomlem  42424  zaddcom  42425  cnreeu  42451  dffltz  42595  cu3addd  42642  3cubeslem2  42646  3cubeslem3l  42647  3cubeslem3r  42648  3cubeslem4  42650  pellexlem2  42791  pellexlem6  42795  pell1234qrreccl  42815  pell1234qrmulcl  42816  pell14qrdich  42830  rmxyneg  42882  rmxyadd  42883  jm2.19lem4  42954  jm2.26lem3  42963  sqrtcval  43603  int-rightdistd  44142  binomcxplemnn0  44311  binomcxplemrat  44312  binomcxplemfrat  44313  binomcxplemdvbinom  44315  binomcxplemnotnn0  44318  sub2times  45244  clim1fr1  45572  limcperiod  45599  addlimc  45619  coseq0  45835  fprodaddrecnncnvlem  45880  dvxpaek  45911  dvnxpaek  45913  dvnmul  45914  itgiccshift  45951  itgperiod  45952  stoweidlem1  45972  stoweidlem11  45982  stoweidlem13  45984  wallispilem4  46039  wallispilem5  46040  wallispi  46041  wallispi2lem1  46042  wallispi2lem2  46043  wallispi2  46044  stirlinglem1  46045  stirlinglem3  46047  stirlinglem4  46048  stirlinglem5  46049  stirlinglem6  46050  stirlinglem7  46051  stirlinglem10  46054  stirlinglem11  46055  stirlinglem12  46056  stirlinglem13  46057  stirlinglem15  46059  dirkerper  46067  dirkertrigeqlem1  46069  dirkertrigeqlem2  46070  dirkertrigeqlem3  46071  dirkeritg  46073  dirkercncflem2  46075  dirkercncflem4  46077  fourierdlem18  46096  fourierdlem26  46104  fourierdlem30  46108  fourierdlem48  46125  fourierdlem49  46126  fourierdlem79  46156  fourierdlem83  46160  fourierdlem92  46169  fourierdlem93  46170  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fourierdlem112  46189  smfmullem1  46762  sigaraf  46824  sigaras  46826  readdcnnred  47277  fldivmod  47312  fmtnorec4  47523  quad1  47594  requad01  47595  requad2  47597  gpgedgvtx1  48026  dignn0flhalflem1  48577  affinecomb2  48665  eenglngeehlnmlem1  48699  itschlc0yqe  48722  itsclc0yqsollem1  48724  itsclc0yqsol  48726  itscnhlc0xyqsol  48727  itsclc0xyqsolr  48731  2itscplem3  48742  itscnhlinecirc02plem1  48744  inlinecirc02plem  48748  sinhpcosh  49702