Theorem addcld 11255

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

Syntax hints:   → wi 4   ∈ wcel 2099  (class class class)co 7414  ℂcc 11128   + caddc 11133

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

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

This theorem is referenced by:  cnegex  11417  addcom  11422  addcomd  11438  muladd11r  11449  negeu  11472  addsubass  11492  subsub2  11510  subsub4  11515  pnncan  11523  addsub4  11525  pnpncand  11657  addmulsub  11698  subaddmulsub  11699  mulsubaddmulsub  11700  divdir  11919  cju  12230  cnref1o  12991  xov1plusxeqvd  13499  expaddz  14095  binom3  14210  sqoddm1div8  14229  mulsubdivbinom2  14245  muldivbinom2  14246  spllen  14728  crre  15085  remullem  15099  imval2  15122  cjreim2  15132  sqreulem  15330  bhmafibid1cn  15434  bhmafibid2cn  15435  bhmafibid1  15436  bhmafibid2  15437  addcn2  15562  o1add  15582  rlimadd  15611  fsumadd  15710  isumadd  15737  binomlem  15799  binomfallfaclem2  16008  bpoly4  16027  fsumcube  16028  efaddlem  16061  ef4p  16081  cosf  16093  tanval2  16101  tanval3  16102  resin4p  16106  recos4p  16107  efival  16120  sinadd  16132  cosadd  16133  tanadd  16135  pwp1fsum  16359  sadadd2lem2  16416  sadadd2lem  16425  pythagtriplem1  16776  pythagtriplem12  16786  pythagtriplem17  16791  pcbc  16860  mul4sqlem  16913  4sqlem14  16918  vdwlem6  16946  vdwlem9  16949  mulgdirlem  19051  blcvx  24701  cphpyth  25131  tcphcphlem1  25150  cphipval2  25156  4cphipval2  25157  csbren  25314  ovollb2lem  25404  mbfadd  25577  itgcnlem  25706  itgaddlem2  25740  dvmptre  25888  dvsincos  25900  itgpowd  25972  taylthlem2  26296  taylthlem2OLD  26297  ptolemy  26418  tanregt0  26460  eff1olem  26469  cosargd  26529  tanarg  26540  logf1o2  26571  efopn  26579  cxpsqrtlem  26623  cxpeq  26679  ang180lem1  26728  ang180lem2  26729  ang180lem3  26730  ang180lem4  26731  pythag  26736  ssscongptld  26741  chordthmlem  26751  chordthmlem2  26752  chordthmlem3  26753  chordthmlem4  26754  chordthmlem5  26755  heron  26757  quad2  26758  dcubic1lem  26762  dcubic2  26763  dcubic1  26764  dcubic  26765  mcubic  26766  cubic2  26767  cubic  26768  binom4  26769  dquartlem1  26770  dquartlem2  26771  dquart  26772  quart1cl  26773  quart1lem  26774  quart1  26775  quartlem1  26776  quartlem2  26777  quartlem3  26778  quartlem4  26779  quart  26780  asinlem3  26790  asinf  26791  asinneg  26805  efiasin  26807  asinsinlem  26810  asinsin  26811  asinbnd  26818  atanlogaddlem  26832  dmgmaddnn0  26946  dmgmdivn0  26947  lgamgulmlem2  26949  lgamgulmlem3  26950  lgamgulmlem4  26951  lgamgulmlem5  26952  lgamgulmlem6  26953  lgamgulm2  26955  lgambdd  26956  lgamucov  26957  lgamcvg2  26974  gamcvg  26975  gamcvg2lem  26978  ftalem7  26998  basellem3  27002  bposlem9  27212  lgsquad2lem1  27304  2lgslem3d1  27323  2sqmod  27356  dchrvmasumiflem2  27422  mulogsumlem  27451  mulog2sumlem1  27454  mulog2sumlem2  27455  mulog2sumlem3  27456  selberglem1  27465  selberg2  27471  selberg3lem1  27477  selbergr  27488  selberg3r  27489  pntrlog2bndlem1  27497  pntrlog2bndlem2  27498  pntrlog2bndlem5  27501  pntrlog2bndlem6  27503  pntrlog2bnd  27504  brbtwn2  28703  colinearalglem1  28704  colinearalglem2  28705  axeuclidlem  28760  axcontlem2  28763  axcontlem7  28768  axcontlem8  28769  finsumvtxdg2ssteplem4  29349  wwlksext2clwwlk  29854  4ipval2  30505  dipcj  30511  golem1  32068  lt2addrd  32505  cycpmco2lem3  32827  cycpmco2lem4  32828  cycpmco2lem5  32829  cycpmco2lem6  32830  cycpmco2  32832  archirngz  32875  archiabllem2c  32881  ccfldextdgrr  33292  cnre2csqima  33448  ballotlemsima  34071  hgt750lemb  34224  iprodgam  35272  dnizphlfeqhlf  35887  dnibndlem9  35897  knoppndvlem16  35938  itg2addnclem3  37081  itgaddnclem2  37087  itgaddnc  37088  ftc1anclem6  37106  ftc1anclem8  37108  dvasin  37112  areacirclem1  37116  areacirclem4  37119  areacirc  37121  lcmineqlem6  41442  lcmineqlem11  41447  lcmineqlem18  41454  aks4d1p1p2  41478  aks4d1p1p6  41481  aks4d1p1p7  41482  aks4d1p1p5  41483  posbezout  41507  2np3bcnp1  41548  2ap1caineq  41549  sticksstones12a  41561  metakunt29  41605  mvrrsubd  41771  lsubrotld  41774  oddnumth  41793  sumcubes  41795  cxp112d  41834  cxp111d  41835  sn-negex12  41893  sn-addrid  41897  sn-subeu  41903  sn-0tie0  41916  zaddcomlem  41928  zaddcom  41929  cnreeu  41945  dffltz  41980  cu3addd  42022  3cubeslem2  42027  3cubeslem3l  42028  3cubeslem3r  42029  3cubeslem4  42031  pellexlem2  42172  pellexlem6  42176  pell1234qrreccl  42196  pell1234qrmulcl  42197  pell14qrdich  42211  rmxyneg  42263  rmxyadd  42264  jm2.19lem4  42335  jm2.26lem3  42344  sqrtcval  42994  int-rightdistd  43533  binomcxplemnn0  43709  binomcxplemrat  43710  binomcxplemfrat  43711  binomcxplemdvbinom  43713  binomcxplemnotnn0  43716  sub2times  44577  clim1fr1  44912  limcperiod  44939  addlimc  44959  coseq0  45175  fprodaddrecnncnvlem  45220  dvxpaek  45251  dvnxpaek  45253  dvnmul  45254  itgiccshift  45291  itgperiod  45292  stoweidlem1  45312  stoweidlem11  45322  stoweidlem13  45324  wallispilem4  45379  wallispilem5  45380  wallispi  45381  wallispi2lem1  45382  wallispi2lem2  45383  wallispi2  45384  stirlinglem1  45385  stirlinglem3  45387  stirlinglem4  45388  stirlinglem5  45389  stirlinglem6  45390  stirlinglem7  45391  stirlinglem10  45394  stirlinglem11  45395  stirlinglem12  45396  stirlinglem13  45397  stirlinglem15  45399  dirkerper  45407  dirkertrigeqlem1  45409  dirkertrigeqlem2  45410  dirkertrigeqlem3  45411  dirkeritg  45413  dirkercncflem2  45415  dirkercncflem4  45417  fourierdlem18  45436  fourierdlem26  45444  fourierdlem30  45448  fourierdlem48  45465  fourierdlem49  45466  fourierdlem79  45496  fourierdlem83  45500  fourierdlem92  45509  fourierdlem93  45510  fourierdlem103  45520  fourierdlem104  45521  fourierdlem111  45528  fourierdlem112  45529  smfmullem1  46102  sigaraf  46164  sigaras  46166  readdcnnred  46606  fmtnorec4  46812  quad1  46883  requad01  46884  requad2  46886  fldivmod  47514  dignn0flhalflem1  47611  affinecomb2  47699  eenglngeehlnmlem1  47733  itschlc0yqe  47756  itsclc0yqsollem1  47758  itsclc0yqsol  47760  itscnhlc0xyqsol  47761  itsclc0xyqsolr  47765  2itscplem3  47776  itscnhlinecirc02plem1  47778  inlinecirc02plem  47782  sinhpcosh  48094