Theorem addcld 11321

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7418  ℂcc 11191   + caddc 11196

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addcl 11253

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  cnegex  11484  addcom  11489  addcomd  11505  muladd11r  11516  negeu  11540  addsubass  11560  subsub2  11579  subsub4  11584  pnncan  11592  addsub4  11594  addsubsub23  11715  mvrrsubd  11722  pnpncand  11730  addmulsub  11771  subaddmulsub  11772  mulsubaddmulsub  11773  divdir  11992  cju  12309  cnref1o  13106  xov1plusxeqvd  13622  modaddb  14042  expaddz  14242  binom3  14361  sqoddm1div8  14380  mulsubdivbinom2  14399  muldivbinom2  14400  spllen  14896  crre  15274  remullem  15288  imval2  15311  cjreim2  15321  sqreulem  15520  bhmafibid1cn  15626  bhmafibid2cn  15627  bhmafibid1  15628  bhmafibid2  15629  addcn2  15754  o1add  15774  rlimadd  15803  fsumadd  15899  isumadd  15926  binomlem  15991  binomfallfaclem2  16199  bpoly4  16218  fsumcube  16219  efaddlem  16252  ef4p  16274  cosf  16286  tanval2  16294  tanval3  16295  resin4p  16299  recos4p  16300  efival  16313  sinadd  16325  cosadd  16326  tanadd  16328  pwp1fsum  16554  sadadd2lem2  16613  sadadd2lem  16622  pythagtriplem1  16987  pythagtriplem12  16997  pythagtriplem17  17002  pcbc  17071  mul4sqlem  17124  4sqlem14  17129  vdwlem6  17157  vdwlem9  17160  mulgdirlem  19308  blcvx  25110  cphpyth  25530  tcphcphlem1  25549  cphipval2  25555  4cphipval2  25556  csbren  25713  ovollb2lem  25802  mbfadd  25975  itgcnlem  26103  itgaddlem2  26137  dvmptre  26282  dvsincos  26294  itgpowd  26363  taylthlem2  26694  ptolemy  26818  tanregt0  26860  eff1olem  26869  cosargd  26929  tanarg  26940  logf1o2  26971  efopn  26979  cxpsqrtlem  27023  cxpeq  27078  ang180lem1  27130  ang180lem2  27131  ang180lem3  27132  ang180lem4  27133  pythag  27138  ssscongptld  27143  chordthmlem  27153  chordthmlem2  27154  chordthmlem3  27155  chordthmlem4  27156  chordthmlem5  27157  heron  27159  quad2  27160  dcubic1lem  27164  dcubic2  27165  dcubic1  27166  dcubic  27167  mcubic  27168  cubic2  27169  cubic  27170  binom4  27171  dquartlem1  27172  dquartlem2  27173  dquart  27174  quart1cl  27175  quart1lem  27176  quart1  27177  quartlem1  27178  quartlem2  27179  quartlem3  27180  quartlem4  27181  quart  27182  asinlem3  27192  asinf  27193  asinneg  27207  efiasin  27209  asinsinlem  27212  asinsin  27213  asinbnd  27220  atanlogaddlem  27234  dmgmaddnn0  27347  dmgmdivn0  27348  lgamgulmlem2  27350  lgamgulmlem3  27351  lgamgulmlem4  27352  lgamgulmlem5  27353  lgamgulmlem6  27354  lgamgulm2  27356  lgambdd  27357  lgamucov  27358  lgamcvg2  27375  gamcvg  27376  gamcvg2lem  27379  ftalem7  27399  basellem3  27403  bposlem9  27612  lgsquad2lem1  27704  2lgslem3d1  27723  2sqmod  27756  dchrvmasumiflem2  27822  mulogsumlem  27851  mulog2sumlem1  27854  mulog2sumlem2  27855  mulog2sumlem3  27856  selberglem1  27865  selberg2  27871  selberg3lem1  27877  selbergr  27888  selberg3r  27889  pntrlog2bndlem1  27897  pntrlog2bndlem2  27898  pntrlog2bndlem5  27901  pntrlog2bndlem6  27903  pntrlog2bnd  27904  brbtwn2  29476  colinearalglem1  29477  colinearalglem2  29478  axeuclidlem  29533  axcontlem2  29536  axcontlem7  29541  axcontlem8  29542  finsumvtxdg2ssteplem4  30122  wwlksext2clwwlk  30641  4ipval2  31303  dipcj  31309  golem1  32866  submuladdd  33325  binom2subadd  33326  pythagreim  33330  quad3d  33334  lt2addrd  33335  cycpmco2lem3  33682  cycpmco2lem4  33683  cycpmco2lem5  33684  cycpmco2lem6  33685  cycpmco2  33687  archirngz  33743  archiabllem2c  33749  zringfrac  34079  ccfldextdgrr  34297  constrrtll  34356  constrrtlc1  34357  constrrtcclem  34359  constrrtcc  34360  constrfin  34371  nn0constr  34386  constraddcl  34387  constrrecl  34394  constrresqrtcl  34402  constrsqrtcl  34404  cos9thpiminplylem1  34407  cos9thpiminplylem2  34408  cos9thpiminplylem3  34409  cos9thpiminply  34413  cos9thpinconstrlem1  34414  cos9thpinconstrlem2  34415  cnre2csqima  34536  ballotlemsima  35141  hgt750lemb  35278  iprodgam  36486  dnizphlfeqhlf  37322  dnibndlem9  37332  knoppndvlem16  37373  qdiff  38228  itg2addnclem3  38571  itgaddnclem2  38577  itgaddnc  38578  ftc1anclem6  38596  ftc1anclem8  38598  dvasin  38602  areacirclem1  38606  areacirclem4  38609  areacirc  38611  lcmineqlem6  43064  lcmineqlem11  43069  lcmineqlem18  43076  aks4d1p1p2  43100  aks4d1p1p6  43103  aks4d1p1p7  43104  aks4d1p1p5  43105  posbezout  43130  2np3bcnp1  43174  2ap1caineq  43175  sticksstones12a  43187  bcle2d  43209  quadfac  43235  lsubrotld  43314  oddnumth  43348  sumcubes  43350  cxp112d  43372  cxp111d  43373  sn-negex12  43448  sn-addrid  43452  sn-subeu  43458  sn-0tie0  43495  zaddcomlem  43507  zaddcom  43508  cnreeu  43534  dffltz  43650  cu3addd  43671  3cubeslem2  43675  3cubeslem3l  43676  3cubeslem3r  43677  3cubeslem4  43679  pellexlem2  43816  pellexlem6  43820  pell1234qrreccl  43840  pell1234qrmulcl  43841  pell14qrdich  43855  rmxyneg  43906  rmxyadd  43907  jm2.19lem4  43978  jm2.26lem3  43987  sqrtcval  44626  int-rightdistd  45165  binomcxplemnn0  45318  binomcxplemrat  45319  binomcxplemfrat  45320  binomcxplemdvbinom  45322  binomcxplemnotnn0  45325  sub2times  46258  clim1fr1  46582  limcperiod  46609  addlimc  46627  coseq0  46843  fprodaddrecnncnvlem  46888  dvxpaek  46919  dvnxpaek  46921  dvnmul  46922  itgiccshift  46959  itgperiod  46960  stoweidlem1  46980  stoweidlem11  46990  stoweidlem13  46992  wallispilem4  47047  wallispilem5  47048  wallispi  47049  wallispi2lem1  47050  wallispi2lem2  47051  wallispi2  47052  stirlinglem1  47053  stirlinglem3  47055  stirlinglem4  47056  stirlinglem5  47057  stirlinglem6  47058  stirlinglem7  47059  stirlinglem10  47062  stirlinglem11  47063  stirlinglem12  47064  stirlinglem13  47065  stirlinglem15  47067  dirkerper  47075  dirkertrigeqlem1  47077  dirkertrigeqlem2  47078  dirkertrigeqlem3  47079  dirkeritg  47081  dirkercncflem2  47083  dirkercncflem4  47085  fourierdlem18  47104  fourierdlem26  47112  fourierdlem30  47116  fourierdlem48  47133  fourierdlem49  47134  fourierdlem79  47164  fourierdlem83  47168  fourierdlem92  47177  fourierdlem93  47178  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  fourierdlem112  47197  smfmullem1  47770  sigaraf  47832  sigaras  47834  sin5tlem1  47888  sin5tlem4  47891  sin5tlem5  47892  readdcnnred  48342  fldivmod  48383  fmtnorec4  48603  quad1  48687  requad01  48688  requad2  48690  gpgedgvtx1  49129  dignn0flhalflem1  49696  affinecomb2  49784  eenglngeehlnmlem1  49818  itschlc0yqe  49841  itsclc0yqsollem1  49843  itsclc0yqsol  49845  itscnhlc0xyqsol  49846  itsclc0xyqsolr  49850  2itscplem3  49861  itscnhlinecirc02plem1  49863  inlinecirc02plem  49867  sinhpcosh  50802  crossp3d  50936  veroquadgsumlem  50952