Theorem addcld 11309

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187

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

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

This theorem is referenced by:  cnegex  11471  addcom  11476  addcomd  11492  muladd11r  11503  negeu  11526  addsubass  11546  subsub2  11564  subsub4  11569  pnncan  11577  addsub4  11579  pnpncand  11711  addmulsub  11752  subaddmulsub  11753  mulsubaddmulsub  11754  divdir  11974  cju  12289  cnref1o  13050  xov1plusxeqvd  13558  expaddz  14157  binom3  14273  sqoddm1div8  14292  mulsubdivbinom2  14311  muldivbinom2  14312  spllen  14802  crre  15163  remullem  15177  imval2  15200  cjreim2  15210  sqreulem  15408  bhmafibid1cn  15512  bhmafibid2cn  15513  bhmafibid1  15514  bhmafibid2  15515  addcn2  15640  o1add  15660  rlimadd  15689  fsumadd  15788  isumadd  15815  binomlem  15877  binomfallfaclem2  16088  bpoly4  16107  fsumcube  16108  efaddlem  16141  ef4p  16161  cosf  16173  tanval2  16181  tanval3  16182  resin4p  16186  recos4p  16187  efival  16200  sinadd  16212  cosadd  16213  tanadd  16215  pwp1fsum  16439  sadadd2lem2  16496  sadadd2lem  16505  pythagtriplem1  16863  pythagtriplem12  16873  pythagtriplem17  16878  pcbc  16947  mul4sqlem  17000  4sqlem14  17005  vdwlem6  17033  vdwlem9  17036  mulgdirlem  19145  blcvx  24839  cphpyth  25269  tcphcphlem1  25288  cphipval2  25294  4cphipval2  25295  csbren  25452  ovollb2lem  25542  mbfadd  25715  itgcnlem  25845  itgaddlem2  25879  dvmptre  26027  dvsincos  26039  itgpowd  26111  taylthlem2  26434  taylthlem2OLD  26435  ptolemy  26556  tanregt0  26599  eff1olem  26608  cosargd  26668  tanarg  26679  logf1o2  26710  efopn  26718  cxpsqrtlem  26762  cxpeq  26818  ang180lem1  26870  ang180lem2  26871  ang180lem3  26872  ang180lem4  26873  pythag  26878  ssscongptld  26883  chordthmlem  26893  chordthmlem2  26894  chordthmlem3  26895  chordthmlem4  26896  chordthmlem5  26897  heron  26899  quad2  26900  dcubic1lem  26904  dcubic2  26905  dcubic1  26906  dcubic  26907  mcubic  26908  cubic2  26909  cubic  26910  binom4  26911  dquartlem1  26912  dquartlem2  26913  dquart  26914  quart1cl  26915  quart1lem  26916  quart1  26917  quartlem1  26918  quartlem2  26919  quartlem3  26920  quartlem4  26921  quart  26922  asinlem3  26932  asinf  26933  asinneg  26947  efiasin  26949  asinsinlem  26952  asinsin  26953  asinbnd  26960  atanlogaddlem  26974  dmgmaddnn0  27088  dmgmdivn0  27089  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem4  27093  lgamgulmlem5  27094  lgamgulmlem6  27095  lgamgulm2  27097  lgambdd  27098  lgamucov  27099  lgamcvg2  27116  gamcvg  27117  gamcvg2lem  27120  ftalem7  27140  basellem3  27144  bposlem9  27354  lgsquad2lem1  27446  2lgslem3d1  27465  2sqmod  27498  dchrvmasumiflem2  27564  mulogsumlem  27593  mulog2sumlem1  27596  mulog2sumlem2  27597  mulog2sumlem3  27598  selberglem1  27607  selberg2  27613  selberg3lem1  27619  selbergr  27630  selberg3r  27631  pntrlog2bndlem1  27639  pntrlog2bndlem2  27640  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntrlog2bnd  27646  brbtwn2  28938  colinearalglem1  28939  colinearalglem2  28940  axeuclidlem  28995  axcontlem2  28998  axcontlem7  29003  axcontlem8  29004  finsumvtxdg2ssteplem4  29584  wwlksext2clwwlk  30089  4ipval2  30740  dipcj  30746  golem1  32303  submuladdd  32753  quad3d  32757  lt2addrd  32758  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2  33126  archirngz  33169  archiabllem2c  33175  zringfrac  33547  ccfldextdgrr  33682  constrrtll  33722  constrrtlc1  33723  constrrtcclem  33725  constrrtcc  33726  constrfin  33736  cnre2csqima  33857  ballotlemsima  34480  hgt750lemb  34633  iprodgam  35704  dnizphlfeqhlf  36442  dnibndlem9  36452  knoppndvlem16  36493  itg2addnclem3  37633  itgaddnclem2  37639  itgaddnc  37640  ftc1anclem6  37658  ftc1anclem8  37660  dvasin  37664  areacirclem1  37668  areacirclem4  37671  areacirc  37673  lcmineqlem6  41991  lcmineqlem11  41996  lcmineqlem18  42003  aks4d1p1p2  42027  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  posbezout  42057  2np3bcnp1  42101  2ap1caineq  42102  sticksstones12a  42114  bcle2d  42136  metakunt29  42190  mvrrsubd  42263  lsubrotld  42266  oddnumth  42299  sumcubes  42301  cxp112d  42329  cxp111d  42330  sn-negex12  42392  sn-addrid  42396  sn-subeu  42402  sn-0tie0  42415  zaddcomlem  42427  zaddcom  42428  cnreeu  42446  dffltz  42589  cu3addd  42636  3cubeslem2  42641  3cubeslem3l  42642  3cubeslem3r  42643  3cubeslem4  42645  pellexlem2  42786  pellexlem6  42790  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell14qrdich  42825  rmxyneg  42877  rmxyadd  42878  jm2.19lem4  42949  jm2.26lem3  42958  sqrtcval  43603  int-rightdistd  44142  binomcxplemnn0  44318  binomcxplemrat  44319  binomcxplemfrat  44320  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  sub2times  45187  clim1fr1  45522  limcperiod  45549  addlimc  45569  coseq0  45785  fprodaddrecnncnvlem  45830  dvxpaek  45861  dvnxpaek  45863  dvnmul  45864  itgiccshift  45901  itgperiod  45902  stoweidlem1  45922  stoweidlem11  45932  stoweidlem13  45934  wallispilem4  45989  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  wallispi2  45994  stirlinglem1  45995  stirlinglem3  45997  stirlinglem4  45998  stirlinglem5  45999  stirlinglem6  46000  stirlinglem7  46001  stirlinglem10  46004  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  stirlinglem15  46009  dirkerper  46017  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkeritg  46023  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem18  46046  fourierdlem26  46054  fourierdlem30  46058  fourierdlem48  46075  fourierdlem49  46076  fourierdlem79  46106  fourierdlem83  46110  fourierdlem92  46119  fourierdlem93  46120  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  smfmullem1  46712  sigaraf  46774  sigaras  46776  readdcnnred  47218  fmtnorec4  47423  quad1  47494  requad01  47495  requad2  47497  fldivmod  48252  dignn0flhalflem1  48349  affinecomb2  48437  eenglngeehlnmlem1  48471  itschlc0yqe  48494  itsclc0yqsollem1  48496  itsclc0yqsol  48498  itscnhlc0xyqsol  48499  itsclc0xyqsolr  48503  2itscplem3  48514  itscnhlinecirc02plem1  48516  inlinecirc02plem  48520  sinhpcosh  48832