Theorem addcld 11003

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   + caddc 10883

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

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

This theorem is referenced by:  cnegex  11165  addcom  11170  addcomd  11186  muladd11r  11197  negeu  11220  addsubass  11240  subsub2  11258  subsub4  11263  pnncan  11271  addsub4  11273  pnpncand  11405  addmulsub  11446  subaddmulsub  11447  mulsubaddmulsub  11448  divdir  11667  cju  11978  cnref1o  12734  xov1plusxeqvd  13239  expaddz  13836  binom3  13948  sqoddm1div8  13967  mulsubdivbinom2  13985  muldivbinom2  13986  spllen  14476  crre  14834  remullem  14848  imval2  14871  cjreim2  14881  sqreulem  15080  bhmafibid1cn  15184  bhmafibid2cn  15185  bhmafibid1  15186  bhmafibid2  15187  addcn2  15312  o1add  15332  rlimadd  15361  fsumadd  15461  isumadd  15488  binomlem  15550  binomfallfaclem2  15759  bpoly4  15778  fsumcube  15779  efaddlem  15811  ef4p  15831  cosf  15843  tanval2  15851  tanval3  15852  resin4p  15856  recos4p  15857  efival  15870  sinadd  15882  cosadd  15883  tanadd  15885  pwp1fsum  16109  sadadd2lem2  16166  sadadd2lem  16175  pythagtriplem1  16526  pythagtriplem12  16536  pythagtriplem17  16541  pcbc  16610  mul4sqlem  16663  4sqlem14  16668  vdwlem6  16696  vdwlem9  16699  mulgdirlem  18743  blcvx  23970  cphpyth  24389  tcphcphlem1  24408  cphipval2  24414  4cphipval2  24415  csbren  24572  ovollb2lem  24661  mbfadd  24834  itgcnlem  24963  itgaddlem2  24997  dvmptre  25142  dvsincos  25154  itgpowd  25223  taylthlem2  25542  ptolemy  25662  tanregt0  25704  eff1olem  25713  cosargd  25772  tanarg  25783  logf1o2  25814  efopn  25822  cxpsqrtlem  25866  cxpeq  25919  ang180lem1  25968  ang180lem2  25969  ang180lem3  25970  ang180lem4  25971  pythag  25976  ssscongptld  25981  chordthmlem  25991  chordthmlem2  25992  chordthmlem3  25993  chordthmlem4  25994  chordthmlem5  25995  heron  25997  quad2  25998  dcubic1lem  26002  dcubic2  26003  dcubic1  26004  dcubic  26005  mcubic  26006  cubic2  26007  cubic  26008  binom4  26009  dquartlem1  26010  dquartlem2  26011  dquart  26012  quart1cl  26013  quart1lem  26014  quart1  26015  quartlem1  26016  quartlem2  26017  quartlem3  26018  quartlem4  26019  quart  26020  asinlem3  26030  asinf  26031  asinneg  26045  efiasin  26047  asinsinlem  26050  asinsin  26051  asinbnd  26058  atanlogaddlem  26072  dmgmaddnn0  26185  dmgmdivn0  26186  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem4  26190  lgamgulmlem5  26191  lgamgulmlem6  26192  lgamgulm2  26194  lgambdd  26195  lgamucov  26196  lgamcvg2  26213  gamcvg  26214  gamcvg2lem  26217  ftalem7  26237  basellem3  26241  bposlem9  26449  lgsquad2lem1  26541  2lgslem3d1  26560  2sqmod  26593  dchrvmasumiflem2  26659  mulogsumlem  26688  mulog2sumlem1  26691  mulog2sumlem2  26692  mulog2sumlem3  26693  selberglem1  26702  selberg2  26708  selberg3lem1  26714  selbergr  26725  selberg3r  26726  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntrlog2bnd  26741  brbtwn2  27282  colinearalglem1  27283  colinearalglem2  27284  axeuclidlem  27339  axcontlem2  27342  axcontlem7  27347  axcontlem8  27348  finsumvtxdg2ssteplem4  27924  wwlksext2clwwlk  28430  4ipval2  29079  dipcj  29085  golem1  30642  lt2addrd  31083  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2  31409  archirngz  31452  archiabllem2c  31458  ccfldextdgrr  31751  cnre2csqima  31870  ballotlemsima  32491  hgt750lemb  32645  iprodgam  33717  dnizphlfeqhlf  34665  dnibndlem9  34675  knoppndvlem16  34716  itg2addnclem3  35839  itgaddnclem2  35845  itgaddnc  35846  ftc1anclem6  35864  ftc1anclem8  35866  dvasin  35870  areacirclem1  35874  areacirclem4  35877  areacirc  35879  lcmineqlem6  40049  lcmineqlem11  40054  lcmineqlem18  40061  aks4d1p1p2  40085  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  2np3bcnp1  40107  2ap1caineq  40108  sticksstones12a  40120  metakunt29  40160  mvrrsubd  40310  lsubrotld  40313  sn-negex12  40405  sn-addid1  40409  sn-subeu  40415  sn-0tie0  40428  cnreeu  40445  dffltz  40478  cu3addd  40509  3cubeslem2  40514  3cubeslem3l  40515  3cubeslem3r  40516  3cubeslem4  40518  pellexlem2  40659  pellexlem6  40663  pell1234qrreccl  40683  pell1234qrmulcl  40684  pell14qrdich  40698  rmxyneg  40749  rmxyadd  40750  jm2.19lem4  40821  jm2.26lem3  40830  sqrtcval  41256  int-rightdistd  41798  binomcxplemnn0  41974  binomcxplemrat  41975  binomcxplemfrat  41976  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  sub2times  42820  clim1fr1  43149  limcperiod  43176  addlimc  43196  coseq0  43412  fprodaddrecnncnvlem  43457  dvxpaek  43488  dvnxpaek  43490  dvnmul  43491  itgiccshift  43528  itgperiod  43529  stoweidlem1  43549  stoweidlem11  43559  stoweidlem13  43561  wallispilem4  43616  wallispilem5  43617  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  wallispi2  43621  stirlinglem1  43622  stirlinglem3  43624  stirlinglem4  43625  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem10  43631  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  stirlinglem15  43636  dirkerper  43644  dirkertrigeqlem1  43646  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkeritg  43650  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem18  43673  fourierdlem26  43681  fourierdlem30  43685  fourierdlem48  43702  fourierdlem49  43703  fourierdlem79  43733  fourierdlem83  43737  fourierdlem92  43746  fourierdlem93  43747  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  smfmullem1  44336  sigaraf  44380  sigaras  44382  readdcnnred  44806  fmtnorec4  45012  quad1  45083  requad01  45084  requad2  45086  fldivmod  45875  dignn0flhalflem1  45972  affinecomb2  46060  eenglngeehlnmlem1  46094  itschlc0yqe  46117  itsclc0yqsollem1  46119  itsclc0yqsol  46121  itscnhlc0xyqsol  46122  itsclc0xyqsolr  46126  2itscplem3  46137  itscnhlinecirc02plem1  46139  inlinecirc02plem  46143  sinhpcosh  46453