Theorem addcld 11151

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   + caddc 11029

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

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

This theorem is referenced by:  cnegex  11314  addcom  11319  addcomd  11335  muladd11r  11346  negeu  11370  addsubass  11390  subsub2  11409  subsub4  11414  pnncan  11422  addsub4  11424  addsubsub23  11545  pnpncand  11558  addmulsub  11599  subaddmulsub  11600  mulsubaddmulsub  11601  divdir  11821  cju  12141  cnref1o  12898  xov1plusxeqvd  13414  modaddb  13829  expaddz  14029  binom3  14147  sqoddm1div8  14166  mulsubdivbinom2  14185  muldivbinom2  14186  spllen  14677  crre  15037  remullem  15051  imval2  15074  cjreim2  15084  sqreulem  15283  bhmafibid1cn  15389  bhmafibid2cn  15390  bhmafibid1  15391  bhmafibid2  15392  addcn2  15517  o1add  15537  rlimadd  15566  fsumadd  15663  isumadd  15690  binomlem  15752  binomfallfaclem2  15963  bpoly4  15982  fsumcube  15983  efaddlem  16016  ef4p  16038  cosf  16050  tanval2  16058  tanval3  16059  resin4p  16063  recos4p  16064  efival  16077  sinadd  16089  cosadd  16090  tanadd  16092  pwp1fsum  16318  sadadd2lem2  16377  sadadd2lem  16386  pythagtriplem1  16744  pythagtriplem12  16754  pythagtriplem17  16759  pcbc  16828  mul4sqlem  16881  4sqlem14  16886  vdwlem6  16914  vdwlem9  16917  mulgdirlem  19035  blcvx  24742  cphpyth  25172  tcphcphlem1  25191  cphipval2  25197  4cphipval2  25198  csbren  25355  ovollb2lem  25445  mbfadd  25618  itgcnlem  25747  itgaddlem2  25781  dvmptre  25929  dvsincos  25941  itgpowd  26013  taylthlem2  26338  taylthlem2OLD  26339  ptolemy  26461  tanregt0  26504  eff1olem  26513  cosargd  26573  tanarg  26584  logf1o2  26615  efopn  26623  cxpsqrtlem  26667  cxpeq  26723  ang180lem1  26775  ang180lem2  26776  ang180lem3  26777  ang180lem4  26778  pythag  26783  ssscongptld  26788  chordthmlem  26798  chordthmlem2  26799  chordthmlem3  26800  chordthmlem4  26801  chordthmlem5  26802  heron  26804  quad2  26805  dcubic1lem  26809  dcubic2  26810  dcubic1  26811  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  binom4  26816  dquartlem1  26817  dquartlem2  26818  dquart  26819  quart1cl  26820  quart1lem  26821  quart1  26822  quartlem1  26823  quartlem2  26824  quartlem3  26825  quartlem4  26826  quart  26827  asinlem3  26837  asinf  26838  asinneg  26852  efiasin  26854  asinsinlem  26857  asinsin  26858  asinbnd  26865  atanlogaddlem  26879  dmgmaddnn0  26993  dmgmdivn0  26994  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem4  26998  lgamgulmlem5  26999  lgamgulmlem6  27000  lgamgulm2  27002  lgambdd  27003  lgamucov  27004  lgamcvg2  27021  gamcvg  27022  gamcvg2lem  27025  ftalem7  27045  basellem3  27049  bposlem9  27259  lgsquad2lem1  27351  2lgslem3d1  27370  2sqmod  27403  dchrvmasumiflem2  27469  mulogsumlem  27498  mulog2sumlem1  27501  mulog2sumlem2  27502  mulog2sumlem3  27503  selberglem1  27512  selberg2  27518  selberg3lem1  27524  selbergr  27535  selberg3r  27536  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntrlog2bnd  27551  brbtwn2  28978  colinearalglem1  28979  colinearalglem2  28980  axeuclidlem  29035  axcontlem2  29038  axcontlem7  29043  axcontlem8  29044  finsumvtxdg2ssteplem4  29622  wwlksext2clwwlk  30132  4ipval2  30783  dipcj  30789  golem1  32346  submuladdd  32819  binom2subadd  32821  pythagreim  32825  quad3d  32829  lt2addrd  32830  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2  33215  archirngz  33271  archiabllem2c  33277  zringfrac  33635  ccfldextdgrr  33829  constrrtll  33888  constrrtlc1  33889  constrrtcclem  33891  constrrtcc  33892  constrfin  33903  nn0constr  33918  constraddcl  33919  constrrecl  33926  constrresqrtcl  33934  constrsqrtcl  33936  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminply  33945  cos9thpinconstrlem1  33946  cos9thpinconstrlem2  33947  cnre2csqima  34068  ballotlemsima  34673  hgt750lemb  34813  iprodgam  35936  dnizphlfeqhlf  36676  dnibndlem9  36686  knoppndvlem16  36727  itg2addnclem3  37874  itgaddnclem2  37880  itgaddnc  37881  ftc1anclem6  37899  ftc1anclem8  37901  dvasin  37905  areacirclem1  37909  areacirclem4  37912  areacirc  37914  lcmineqlem6  42288  lcmineqlem11  42293  lcmineqlem18  42300  aks4d1p1p2  42324  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1p5  42329  posbezout  42354  2np3bcnp1  42398  2ap1caineq  42399  sticksstones12a  42411  bcle2d  42433  mvrrsubd  42529  lsubrotld  42532  oddnumth  42566  sumcubes  42568  cxp112d  42596  cxp111d  42597  sn-negex12  42672  sn-addrid  42676  sn-subeu  42682  sn-0tie0  42706  zaddcomlem  42718  zaddcom  42719  cnreeu  42745  dffltz  42877  cu3addd  42923  3cubeslem2  42927  3cubeslem3l  42928  3cubeslem3r  42929  3cubeslem4  42931  pellexlem2  43072  pellexlem6  43076  pell1234qrreccl  43096  pell1234qrmulcl  43097  pell14qrdich  43111  rmxyneg  43162  rmxyadd  43163  jm2.19lem4  43234  jm2.26lem3  43243  sqrtcval  43882  int-rightdistd  44421  binomcxplemnn0  44590  binomcxplemrat  44591  binomcxplemfrat  44592  binomcxplemdvbinom  44594  binomcxplemnotnn0  44597  sub2times  45521  clim1fr1  45847  limcperiod  45874  addlimc  45892  coseq0  46108  fprodaddrecnncnvlem  46153  dvxpaek  46184  dvnxpaek  46186  dvnmul  46187  itgiccshift  46224  itgperiod  46225  stoweidlem1  46245  stoweidlem11  46255  stoweidlem13  46257  wallispilem4  46312  wallispilem5  46313  wallispi  46314  wallispi2lem1  46315  wallispi2lem2  46316  wallispi2  46317  stirlinglem1  46318  stirlinglem3  46320  stirlinglem4  46321  stirlinglem5  46322  stirlinglem6  46323  stirlinglem7  46324  stirlinglem10  46327  stirlinglem11  46328  stirlinglem12  46329  stirlinglem13  46330  stirlinglem15  46332  dirkerper  46340  dirkertrigeqlem1  46342  dirkertrigeqlem2  46343  dirkertrigeqlem3  46344  dirkeritg  46346  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem18  46369  fourierdlem26  46377  fourierdlem30  46381  fourierdlem48  46398  fourierdlem49  46399  fourierdlem79  46429  fourierdlem83  46433  fourierdlem92  46442  fourierdlem93  46443  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem112  46462  smfmullem1  47035  sigaraf  47097  sigaras  47099  readdcnnred  47549  fldivmod  47584  fmtnorec4  47795  quad1  47866  requad01  47867  requad2  47869  gpgedgvtx1  48308  dignn0flhalflem1  48861  affinecomb2  48949  eenglngeehlnmlem1  48983  itschlc0yqe  49006  itsclc0yqsollem1  49008  itsclc0yqsol  49010  itscnhlc0xyqsol  49011  itsclc0xyqsolr  49015  2itscplem3  49026  itscnhlinecirc02plem1  49028  inlinecirc02plem  49032  sinhpcosh  49985