Theorem addcld 11252

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   + caddc 11130

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

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

This theorem is referenced by:  cnegex  11414  addcom  11419  addcomd  11435  muladd11r  11446  negeu  11470  addsubass  11490  subsub2  11509  subsub4  11514  pnncan  11522  addsub4  11524  pnpncand  11656  addmulsub  11697  subaddmulsub  11698  mulsubaddmulsub  11699  divdir  11919  cju  12234  cnref1o  12999  xov1plusxeqvd  13513  expaddz  14122  binom3  14240  sqoddm1div8  14259  mulsubdivbinom2  14278  muldivbinom2  14279  spllen  14770  crre  15131  remullem  15145  imval2  15168  cjreim2  15178  sqreulem  15376  bhmafibid1cn  15480  bhmafibid2cn  15481  bhmafibid1  15482  bhmafibid2  15483  addcn2  15608  o1add  15628  rlimadd  15657  fsumadd  15754  isumadd  15781  binomlem  15843  binomfallfaclem2  16054  bpoly4  16073  fsumcube  16074  efaddlem  16107  ef4p  16129  cosf  16141  tanval2  16149  tanval3  16150  resin4p  16154  recos4p  16155  efival  16168  sinadd  16180  cosadd  16181  tanadd  16183  pwp1fsum  16408  sadadd2lem2  16467  sadadd2lem  16476  pythagtriplem1  16834  pythagtriplem12  16844  pythagtriplem17  16849  pcbc  16918  mul4sqlem  16971  4sqlem14  16976  vdwlem6  17004  vdwlem9  17007  mulgdirlem  19086  blcvx  24735  cphpyth  25166  tcphcphlem1  25185  cphipval2  25191  4cphipval2  25192  csbren  25349  ovollb2lem  25439  mbfadd  25612  itgcnlem  25741  itgaddlem2  25775  dvmptre  25923  dvsincos  25935  itgpowd  26007  taylthlem2  26332  taylthlem2OLD  26333  ptolemy  26455  tanregt0  26498  eff1olem  26507  cosargd  26567  tanarg  26578  logf1o2  26609  efopn  26617  cxpsqrtlem  26661  cxpeq  26717  ang180lem1  26769  ang180lem2  26770  ang180lem3  26771  ang180lem4  26772  pythag  26777  ssscongptld  26782  chordthmlem  26792  chordthmlem2  26793  chordthmlem3  26794  chordthmlem4  26795  chordthmlem5  26796  heron  26798  quad2  26799  dcubic1lem  26803  dcubic2  26804  dcubic1  26805  dcubic  26806  mcubic  26807  cubic2  26808  cubic  26809  binom4  26810  dquartlem1  26811  dquartlem2  26812  dquart  26813  quart1cl  26814  quart1lem  26815  quart1  26816  quartlem1  26817  quartlem2  26818  quartlem3  26819  quartlem4  26820  quart  26821  asinlem3  26831  asinf  26832  asinneg  26846  efiasin  26848  asinsinlem  26851  asinsin  26852  asinbnd  26859  atanlogaddlem  26873  dmgmaddnn0  26987  dmgmdivn0  26988  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem4  26992  lgamgulmlem5  26993  lgamgulmlem6  26994  lgamgulm2  26996  lgambdd  26997  lgamucov  26998  lgamcvg2  27015  gamcvg  27016  gamcvg2lem  27019  ftalem7  27039  basellem3  27043  bposlem9  27253  lgsquad2lem1  27345  2lgslem3d1  27364  2sqmod  27397  dchrvmasumiflem2  27463  mulogsumlem  27492  mulog2sumlem1  27495  mulog2sumlem2  27496  mulog2sumlem3  27497  selberglem1  27506  selberg2  27512  selberg3lem1  27518  selbergr  27529  selberg3r  27530  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  brbtwn2  28830  colinearalglem1  28831  colinearalglem2  28832  axeuclidlem  28887  axcontlem2  28890  axcontlem7  28895  axcontlem8  28896  finsumvtxdg2ssteplem4  29474  wwlksext2clwwlk  29984  4ipval2  30635  dipcj  30641  golem1  32198  submuladdd  32663  binom2subadd  32665  pythagreim  32669  quad3d  32673  lt2addrd  32674  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  archirngz  33133  archiabllem2c  33139  zringfrac  33515  ccfldextdgrr  33659  constrrtll  33711  constrrtlc1  33712  constrrtcclem  33714  constrrtcc  33715  constrfin  33726  nn0constr  33741  constraddcl  33742  constrrecl  33749  constrresqrtcl  33757  constrsqrtcl  33759  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpiminplylem3  33764  cos9thpiminply  33768  cos9thpinconstrlem1  33769  cnre2csqima  33888  ballotlemsima  34494  hgt750lemb  34634  iprodgam  35705  dnizphlfeqhlf  36440  dnibndlem9  36450  knoppndvlem16  36491  itg2addnclem3  37643  itgaddnclem2  37649  itgaddnc  37650  ftc1anclem6  37668  ftc1anclem8  37670  dvasin  37674  areacirclem1  37678  areacirclem4  37681  areacirc  37683  lcmineqlem6  41993  lcmineqlem11  41998  lcmineqlem18  42005  aks4d1p1p2  42029  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  posbezout  42059  2np3bcnp1  42103  2ap1caineq  42104  sticksstones12a  42116  bcle2d  42138  metakunt29  42192  mvrrsubd  42271  lsubrotld  42274  oddnumth  42307  sumcubes  42309  cxp112d  42337  cxp111d  42338  sn-negex12  42406  sn-addrid  42410  sn-subeu  42416  sn-0tie0  42429  zaddcomlem  42441  zaddcom  42442  cnreeu  42460  dffltz  42604  cu3addd  42651  3cubeslem2  42655  3cubeslem3l  42656  3cubeslem3r  42657  3cubeslem4  42659  pellexlem2  42800  pellexlem6  42804  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell14qrdich  42839  rmxyneg  42891  rmxyadd  42892  jm2.19lem4  42963  jm2.26lem3  42972  sqrtcval  43612  int-rightdistd  44151  binomcxplemnn0  44321  binomcxplemrat  44322  binomcxplemfrat  44323  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  sub2times  45249  clim1fr1  45578  limcperiod  45605  addlimc  45625  coseq0  45841  fprodaddrecnncnvlem  45886  dvxpaek  45917  dvnxpaek  45919  dvnmul  45920  itgiccshift  45957  itgperiod  45958  stoweidlem1  45978  stoweidlem11  45988  stoweidlem13  45990  wallispilem4  46045  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  wallispi2  46050  stirlinglem1  46051  stirlinglem3  46053  stirlinglem4  46054  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem10  46060  stirlinglem11  46061  stirlinglem12  46062  stirlinglem13  46063  stirlinglem15  46065  dirkerper  46073  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkeritg  46079  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem18  46102  fourierdlem26  46110  fourierdlem30  46114  fourierdlem48  46131  fourierdlem49  46132  fourierdlem79  46162  fourierdlem83  46166  fourierdlem92  46175  fourierdlem93  46176  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  smfmullem1  46768  sigaraf  46830  sigaras  46832  readdcnnred  47280  fldivmod  47315  fmtnorec4  47511  quad1  47582  requad01  47583  requad2  47585  gpgedgvtx1  48014  dignn0flhalflem1  48543  affinecomb2  48631  eenglngeehlnmlem1  48665  itschlc0yqe  48688  itsclc0yqsollem1  48690  itsclc0yqsol  48692  itscnhlc0xyqsol  48693  itsclc0xyqsolr  48697  2itscplem3  48708  itscnhlinecirc02plem1  48710  inlinecirc02plem  48714  sinhpcosh  49499