Theorem addcld 11195

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

Syntax hints:   → wi 4   ∈ wcel 2141  (class class class)co 7391  ℂcc 11065   + caddc 11070

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

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  cnegex  11358  addcom  11363  addcomd  11379  muladd11r  11390  negeu  11414  addsubass  11434  subsub2  11453  subsub4  11458  pnncan  11466  addsub4  11468  addsubsub23  11589  pnpncand  11602  addmulsub  11643  subaddmulsub  11644  mulsubaddmulsub  11645  divdir  11864  cju  12185  cnref1o  12980  xov1plusxeqvd  13496  modaddb  13913  expaddz  14113  binom3  14231  sqoddm1div8  14250  mulsubdivbinom2  14269  muldivbinom2  14270  spllen  14761  crre  15132  remullem  15146  imval2  15169  cjreim2  15179  sqreulem  15378  bhmafibid1cn  15484  bhmafibid2cn  15485  bhmafibid1  15486  bhmafibid2  15487  addcn2  15612  o1add  15632  rlimadd  15661  fsumadd  15758  isumadd  15785  binomlem  15850  binomfallfaclem2  16061  bpoly4  16080  fsumcube  16081  efaddlem  16114  ef4p  16136  cosf  16148  tanval2  16156  tanval3  16157  resin4p  16161  recos4p  16162  efival  16175  sinadd  16187  cosadd  16188  tanadd  16190  pwp1fsum  16416  sadadd2lem2  16475  sadadd2lem  16484  pythagtriplem1  16843  pythagtriplem12  16853  pythagtriplem17  16858  pcbc  16927  mul4sqlem  16980  4sqlem14  16985  vdwlem6  17013  vdwlem9  17016  mulgdirlem  19138  blcvx  24846  cphpyth  25266  tcphcphlem1  25285  cphipval2  25291  4cphipval2  25292  csbren  25449  ovollb2lem  25538  mbfadd  25711  itgcnlem  25840  itgaddlem2  25874  dvmptre  26019  dvsincos  26031  itgpowd  26100  taylthlem2  26425  ptolemy  26549  tanregt0  26592  eff1olem  26601  cosargd  26661  tanarg  26672  logf1o2  26703  efopn  26711  cxpsqrtlem  26755  cxpeq  26810  ang180lem1  26862  ang180lem2  26863  ang180lem3  26864  ang180lem4  26865  pythag  26870  ssscongptld  26875  chordthmlem  26885  chordthmlem2  26886  chordthmlem3  26887  chordthmlem4  26888  chordthmlem5  26889  heron  26891  quad2  26892  dcubic1lem  26896  dcubic2  26897  dcubic1  26898  dcubic  26899  mcubic  26900  cubic2  26901  cubic  26902  binom4  26903  dquartlem1  26904  dquartlem2  26905  dquart  26906  quart1cl  26907  quart1lem  26908  quart1  26909  quartlem1  26910  quartlem2  26911  quartlem3  26912  quartlem4  26913  quart  26914  asinlem3  26924  asinf  26925  asinneg  26939  efiasin  26941  asinsinlem  26944  asinsin  26945  asinbnd  26952  atanlogaddlem  26966  dmgmaddnn0  27079  dmgmdivn0  27080  lgamgulmlem2  27082  lgamgulmlem3  27083  lgamgulmlem4  27084  lgamgulmlem5  27085  lgamgulmlem6  27086  lgamgulm2  27088  lgambdd  27089  lgamucov  27090  lgamcvg2  27107  gamcvg  27108  gamcvg2lem  27111  ftalem7  27131  basellem3  27135  bposlem9  27344  lgsquad2lem1  27436  2lgslem3d1  27455  2sqmod  27488  dchrvmasumiflem2  27554  mulogsumlem  27583  mulog2sumlem1  27586  mulog2sumlem2  27587  mulog2sumlem3  27588  selberglem1  27597  selberg2  27603  selberg3lem1  27609  selbergr  27620  selberg3r  27621  pntrlog2bndlem1  27629  pntrlog2bndlem2  27630  pntrlog2bndlem5  27633  pntrlog2bndlem6  27635  pntrlog2bnd  27636  brbtwn2  29063  colinearalglem1  29064  colinearalglem2  29065  axeuclidlem  29120  axcontlem2  29123  axcontlem7  29128  axcontlem8  29129  finsumvtxdg2ssteplem4  29706  wwlksext2clwwlk  30216  4ipval2  30868  dipcj  30874  golem1  32431  submuladdd  32903  binom2subadd  32904  pythagreim  32908  quad3d  32912  lt2addrd  32913  cycpmco2lem3  33269  cycpmco2lem4  33270  cycpmco2lem5  33271  cycpmco2lem6  33272  cycpmco2  33274  archirngz  33330  archiabllem2c  33336  zringfrac  33711  ccfldextdgrr  33930  constrrtll  33989  constrrtlc1  33990  constrrtcclem  33992  constrrtcc  33993  constrfin  34004  nn0constr  34019  constraddcl  34020  constrrecl  34027  constrresqrtcl  34035  constrsqrtcl  34037  cos9thpiminplylem1  34040  cos9thpiminplylem2  34041  cos9thpiminplylem3  34042  cos9thpiminply  34046  cos9thpinconstrlem1  34047  cos9thpinconstrlem2  34048  cnre2csqima  34169  ballotlemsima  34774  hgt750lemb  34911  iprodgam  36053  dnizphlfeqhlf  36875  dnibndlem9  36885  knoppndvlem16  36926  qdiff  37780  itg2addnclem3  38133  itgaddnclem2  38139  itgaddnc  38140  ftc1anclem6  38158  ftc1anclem8  38160  dvasin  38164  areacirclem1  38168  areacirclem4  38171  areacirc  38173  lcmineqlem6  42612  lcmineqlem11  42617  lcmineqlem18  42624  aks4d1p1p2  42648  aks4d1p1p6  42651  aks4d1p1p7  42652  aks4d1p1p5  42653  posbezout  42678  2np3bcnp1  42722  2ap1caineq  42723  sticksstones12a  42735  bcle2d  42757  mvrrsubd  42844  lsubrotld  42847  oddnumth  42881  sumcubes  42883  cxp112d  42911  cxp111d  42912  sn-negex12  42987  sn-addrid  42991  sn-subeu  42997  sn-0tie0  43034  zaddcomlem  43046  zaddcom  43047  cnreeu  43073  dffltz  43177  cu3addd  43223  3cubeslem2  43227  3cubeslem3l  43228  3cubeslem3r  43229  3cubeslem4  43231  pellexlem2  43368  pellexlem6  43372  pell1234qrreccl  43392  pell1234qrmulcl  43393  pell14qrdich  43407  rmxyneg  43458  rmxyadd  43459  jm2.19lem4  43530  jm2.26lem3  43539  sqrtcval  44178  int-rightdistd  44717  binomcxplemnn0  44886  binomcxplemrat  44887  binomcxplemfrat  44888  binomcxplemdvbinom  44890  binomcxplemnotnn0  44893  sub2times  45813  clim1fr1  46138  limcperiod  46165  addlimc  46183  coseq0  46399  fprodaddrecnncnvlem  46444  dvxpaek  46475  dvnxpaek  46477  dvnmul  46478  itgiccshift  46515  itgperiod  46516  stoweidlem1  46536  stoweidlem11  46546  stoweidlem13  46548  wallispilem4  46603  wallispilem5  46604  wallispi  46605  wallispi2lem1  46606  wallispi2lem2  46607  wallispi2  46608  stirlinglem1  46609  stirlinglem3  46611  stirlinglem4  46612  stirlinglem5  46613  stirlinglem6  46614  stirlinglem7  46615  stirlinglem10  46618  stirlinglem11  46619  stirlinglem12  46620  stirlinglem13  46621  stirlinglem15  46623  dirkerper  46631  dirkertrigeqlem1  46633  dirkertrigeqlem2  46634  dirkertrigeqlem3  46635  dirkeritg  46637  dirkercncflem2  46639  dirkercncflem4  46641  fourierdlem18  46660  fourierdlem26  46668  fourierdlem30  46672  fourierdlem48  46689  fourierdlem49  46690  fourierdlem79  46720  fourierdlem83  46724  fourierdlem92  46733  fourierdlem93  46734  fourierdlem103  46744  fourierdlem104  46745  fourierdlem111  46752  fourierdlem112  46753  smfmullem1  47326  sigaraf  47388  sigaras  47390  sin5tlem1  47428  sin5tlem4  47431  sin5tlem5  47432  readdcnnred  47858  fldivmod  47899  fmtnorec4  48119  quad1  48203  requad01  48204  requad2  48206  gpgedgvtx1  48645  dignn0flhalflem1  49198  affinecomb2  49286  eenglngeehlnmlem1  49320  itschlc0yqe  49343  itsclc0yqsollem1  49345  itsclc0yqsol  49347  itscnhlc0xyqsol  49348  itsclc0xyqsolr  49352  2itscplem3  49363  itscnhlinecirc02plem1  49365  inlinecirc02plem  49369  sinhpcosh  50322