Theorem addcld 11277

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

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   + caddc 11155

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

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

This theorem is referenced by:  cnegex  11439  addcom  11444  addcomd  11460  muladd11r  11471  negeu  11495  addsubass  11515  subsub2  11534  subsub4  11539  pnncan  11547  addsub4  11549  pnpncand  11681  addmulsub  11722  subaddmulsub  11723  mulsubaddmulsub  11724  divdir  11944  cju  12259  cnref1o  13024  xov1plusxeqvd  13534  expaddz  14143  binom3  14259  sqoddm1div8  14278  mulsubdivbinom2  14297  muldivbinom2  14298  spllen  14788  crre  15149  remullem  15163  imval2  15186  cjreim2  15196  sqreulem  15394  bhmafibid1cn  15498  bhmafibid2cn  15499  bhmafibid1  15500  bhmafibid2  15501  addcn2  15626  o1add  15646  rlimadd  15675  fsumadd  15772  isumadd  15799  binomlem  15861  binomfallfaclem2  16072  bpoly4  16091  fsumcube  16092  efaddlem  16125  ef4p  16145  cosf  16157  tanval2  16165  tanval3  16166  resin4p  16170  recos4p  16171  efival  16184  sinadd  16196  cosadd  16197  tanadd  16199  pwp1fsum  16424  sadadd2lem2  16483  sadadd2lem  16492  pythagtriplem1  16849  pythagtriplem12  16859  pythagtriplem17  16864  pcbc  16933  mul4sqlem  16986  4sqlem14  16991  vdwlem6  17019  vdwlem9  17022  mulgdirlem  19135  blcvx  24833  cphpyth  25263  tcphcphlem1  25282  cphipval2  25288  4cphipval2  25289  csbren  25446  ovollb2lem  25536  mbfadd  25709  itgcnlem  25839  itgaddlem2  25873  dvmptre  26021  dvsincos  26033  itgpowd  26105  taylthlem2  26430  taylthlem2OLD  26431  ptolemy  26552  tanregt0  26595  eff1olem  26604  cosargd  26664  tanarg  26675  logf1o2  26706  efopn  26714  cxpsqrtlem  26758  cxpeq  26814  ang180lem1  26866  ang180lem2  26867  ang180lem3  26868  ang180lem4  26869  pythag  26874  ssscongptld  26879  chordthmlem  26889  chordthmlem2  26890  chordthmlem3  26891  chordthmlem4  26892  chordthmlem5  26893  heron  26895  quad2  26896  dcubic1lem  26900  dcubic2  26901  dcubic1  26902  dcubic  26903  mcubic  26904  cubic2  26905  cubic  26906  binom4  26907  dquartlem1  26908  dquartlem2  26909  dquart  26910  quart1cl  26911  quart1lem  26912  quart1  26913  quartlem1  26914  quartlem2  26915  quartlem3  26916  quartlem4  26917  quart  26918  asinlem3  26928  asinf  26929  asinneg  26943  efiasin  26945  asinsinlem  26948  asinsin  26949  asinbnd  26956  atanlogaddlem  26970  dmgmaddnn0  27084  dmgmdivn0  27085  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem4  27089  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamgulm2  27093  lgambdd  27094  lgamucov  27095  lgamcvg2  27112  gamcvg  27113  gamcvg2lem  27116  ftalem7  27136  basellem3  27140  bposlem9  27350  lgsquad2lem1  27442  2lgslem3d1  27461  2sqmod  27494  dchrvmasumiflem2  27560  mulogsumlem  27589  mulog2sumlem1  27592  mulog2sumlem2  27593  mulog2sumlem3  27594  selberglem1  27603  selberg2  27609  selberg3lem1  27615  selbergr  27626  selberg3r  27627  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntrlog2bnd  27642  brbtwn2  28934  colinearalglem1  28935  colinearalglem2  28936  axeuclidlem  28991  axcontlem2  28994  axcontlem7  28999  axcontlem8  29000  finsumvtxdg2ssteplem4  29580  wwlksext2clwwlk  30085  4ipval2  30736  dipcj  30742  golem1  32299  submuladdd  32756  quad3d  32760  lt2addrd  32761  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2  33135  archirngz  33178  archiabllem2c  33184  zringfrac  33561  ccfldextdgrr  33696  constrrtll  33736  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  constrfin  33750  cnre2csqima  33871  ballotlemsima  34496  hgt750lemb  34649  iprodgam  35721  dnizphlfeqhlf  36458  dnibndlem9  36468  knoppndvlem16  36509  itg2addnclem3  37659  itgaddnclem2  37665  itgaddnc  37666  ftc1anclem6  37684  ftc1anclem8  37686  dvasin  37690  areacirclem1  37694  areacirclem4  37697  areacirc  37699  lcmineqlem6  42015  lcmineqlem11  42020  lcmineqlem18  42027  aks4d1p1p2  42051  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  posbezout  42081  2np3bcnp1  42125  2ap1caineq  42126  sticksstones12a  42138  bcle2d  42160  metakunt29  42214  mvrrsubd  42287  lsubrotld  42290  oddnumth  42323  sumcubes  42325  cxp112d  42355  cxp111d  42356  sn-negex12  42422  sn-addrid  42426  sn-subeu  42432  sn-0tie0  42445  zaddcomlem  42457  zaddcom  42458  cnreeu  42476  dffltz  42620  cu3addd  42667  3cubeslem2  42672  3cubeslem3l  42673  3cubeslem3r  42674  3cubeslem4  42676  pellexlem2  42817  pellexlem6  42821  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell14qrdich  42856  rmxyneg  42908  rmxyadd  42909  jm2.19lem4  42980  jm2.26lem3  42989  sqrtcval  43630  int-rightdistd  44169  binomcxplemnn0  44344  binomcxplemrat  44345  binomcxplemfrat  44346  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  sub2times  45222  clim1fr1  45556  limcperiod  45583  addlimc  45603  coseq0  45819  fprodaddrecnncnvlem  45864  dvxpaek  45895  dvnxpaek  45897  dvnmul  45898  itgiccshift  45935  itgperiod  45936  stoweidlem1  45956  stoweidlem11  45966  stoweidlem13  45968  wallispilem4  46023  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  stirlinglem3  46031  stirlinglem4  46032  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem15  46043  dirkerper  46051  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkeritg  46057  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem18  46080  fourierdlem26  46088  fourierdlem30  46092  fourierdlem48  46109  fourierdlem49  46110  fourierdlem79  46140  fourierdlem83  46144  fourierdlem92  46153  fourierdlem93  46154  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  smfmullem1  46746  sigaraf  46808  sigaras  46810  readdcnnred  47252  fldivmod  47277  fmtnorec4  47473  quad1  47544  requad01  47545  requad2  47547  gpgedgvtx1  47954  dignn0flhalflem1  48464  affinecomb2  48552  eenglngeehlnmlem1  48586  itschlc0yqe  48609  itsclc0yqsollem1  48611  itsclc0yqsol  48613  itscnhlc0xyqsol  48614  itsclc0xyqsolr  48618  2itscplem3  48629  itscnhlinecirc02plem1  48631  inlinecirc02plem  48635  sinhpcosh  48970