Theorem mulid2d 9937

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mulid2d	⊢ (𝜑 → (1 · 𝐴) = 𝐴)

Proof of Theorem mulid2d

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulid2 9917	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813  1c1 9816   · cmul 9820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-mulcom 9879  ax-mulass 9881  ax-distr 9882  ax-1rid 9885  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  adddirp1d  9945  addid1  10095  mulsubfacd  10371  mulcand  10539  receu  10551  divdivdiv  10605  divcan5  10606  subrec  10733  ltrec  10784  recp1lt1  10800  nndivtr  10939  subhalfhalf  11143  xp1d2m1eqxm1d2  11163  gtndiv  11330  lincmb01cmp  12186  iccf1o  12187  ltdifltdiv  12497  modfrac  12545  modvalp1  12551  negmod  12577  addmodid  12580  m1expcl2  12744  expgt1  12760  ltexp2a  12774  leexp2a  12778  binom3  12847  faclbnd  12939  faclbnd4lem4  12945  facavg  12950  bcval5  12967  cshweqrep  13418  sqrlem2  13832  absimle  13897  reccn2  14175  iseraltlem2  14261  iseraltlem3  14262  o1fsum  14386  abscvgcvg  14392  ackbijnn  14399  binom1p  14402  binom1dif  14404  incexclem  14407  incexc  14408  climcndslem1  14420  geomulcvg  14446  fprodsplit  14535  fallrisefac  14595  bpolysum  14623  bpolydiflem  14624  bpoly4  14629  efcllem  14647  ef01bndlem  14753  efieq1re  14768  eirrlem  14771  iddvds  14833  pwp1fsum  14952  oddpwp1fsum  14953  bitsfzolem  14994  bitsfzo  14995  rpmulgcd  15113  prmind2  15236  isprm5  15257  phiprm  15320  eulerthlem2  15325  fermltl  15327  hashgcdlem  15331  odzdvds  15338  powm2modprm  15346  modprm0  15348  pythagtriplem4  15362  pcexp  15402  4sqlem18  15504  vdwapun  15516  mulgnnass  17399  mulgnnassOLD  17400  odinv  17801  odadd2  18075  pgpfaclem2  18304  abvneg  18657  nrginvrcnlem  22305  nmoid  22356  blcvx  22409  icopnfcnv  22549  reparphti  22605  pcorevlem  22634  ncvsm1  22762  ncvspi  22764  cphipval2  22848  cphipval  22850  itg11  23264  itg2mulc  23320  itg2monolem1  23323  itgcnlem  23362  iblabs  23401  dvexp  23522  dvef  23547  lhop1lem  23580  dvcvx  23587  dvfsumlem1  23593  dvfsumlem2  23594  dvfsumlem4  23596  dvfsum2  23601  plypow  23765  dgrcolem1  23833  vieta1lem2  23870  radcnvlem1  23971  radcnvlem2  23972  dvradcnv  23979  abelthlem2  23990  abelthlem6  23994  abelthlem7  23996  abelth2  24000  sinhalfpip  24048  sinhalfpim  24049  coshalfpip  24050  coshalfpim  24051  tangtx  24061  efif1olem4  24095  abslogle  24168  logdivlti  24170  advlog  24200  advlogexp  24201  logtayl  24206  cxpaddlelem  24292  cxpaddle  24293  affineequiv  24353  affineequiv2  24354  chordthmlem5  24363  dcubic2  24371  dcubic  24373  mcubic  24374  binom4  24377  dquartlem1  24378  quart1lem  24382  quart1  24383  quartlem1  24384  quart  24388  efiasin  24415  atantayl  24464  cvxcl  24511  scvxcvx  24512  lgamgulmlem5  24559  lgamcvg2  24581  lgam1  24590  wilthlem1  24594  wilthlem2  24595  basellem9  24615  fsumfldivdiaglem  24715  muinv  24719  chpub  24745  logexprlim  24750  mersenne  24752  perfectlem2  24755  dchrmulid2  24777  dchrptlem1  24789  dchrsum2  24793  sumdchr2  24795  bposlem2  24810  bposlem9  24817  lgsval2lem  24832  lgsval4a  24844  lgsneg1  24847  lgsdir2lem4  24853  lgsdir  24857  lgsmulsqcoprm  24868  lgsdirnn0  24869  lgsdinn0  24870  gausslemma2dlem1a  24890  gausslemma2dlem4  24894  gausslemma2dlem7  24898  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem4  24903  lgsquad2lem1  24909  2sqlem8  24951  chebbnd1lem3  24960  chpchtlim  24968  rplogsumlem1  24973  rplogsumlem2  24974  rpvmasumlem  24976  dchrmusum2  24983  dchrvmasum2lem  24985  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrisum0flblem1  24997  mulog2sumlem2  25024  vmalogdivsum2  25027  2vmadivsumlem  25029  log2sumbnd  25033  selberglem2  25035  chpdifbndlem1  25042  selberg3lem1  25046  selberg4lem1  25049  pntrlog2bndlem2  25067  pntrlog2bndlem5  25070  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2  25080  pntlemb  25086  pntlemr  25091  pntlemk  25095  pntlemo  25096  brbtwn2  25585  colinearalglem4  25589  ax5seglem3  25611  axbtwnid  25619  axpaschlem  25620  axeuclidlem  25642  axcontlem7  25650  axcontlem8  25651  nvm1  26904  nvpi  26906  nvmtri  26910  ipval2  26946  ipasslem1  27070  ipasslem4  27073  bcs2  27423  lnfnaddi  28286  sqsscirc1  29282  indsum  29412  eulerpartlemgs2  29769  plymulx0  29950  subfacp1lem6  30421  subfaclim  30424  cvxpcon  30478  cvxscon  30479  rescon  30482  sinccvglem  30820  fwddifn0  31441  nn0prpwlem  31487  knoppndvlem9  31681  knoppndvlem14  31686  bj-bary1lem1  32338  mblfinlem3  32618  itg2addnclem3  32633  iblabsnc  32644  iblmulc2nc  32645  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  areacirclem1  32670  bfplem2  32792  bfp  32793  rrntotbnd  32805  irrapxlem5  36408  pellexlem2  36412  pellexlem6  36416  pellfundex  36468  jm2.19lem3  36576  jm2.25  36584  jm2.27c  36592  jm3.1lem2  36603  flcidc  36763  int-mul12d  37508  cvgdvgrat  37534  bccn1  37565  binomcxplemnotnn0  37577  fperiodmullem  38458  xralrple2  38511  fmul01lt1lem2  38652  mccllem  38664  reclimc  38720  cosknegpi  38752  dvsinax  38801  dvmptdiv  38807  dvnxpaek  38832  dvnmul  38833  itgsinexp  38846  stoweidlem14  38907  stoweidlem26  38919  wallispilem4  38961  wallispilem5  38962  wallispi2lem1  38964  wallispi2  38966  stirlinglem1  38967  stirlinglem3  38969  stirlinglem4  38970  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkercncflem2  38997  fourierdlem26  39026  fourierdlem41  39041  fourierdlem42  39042  fourierdlem56  39055  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fourierdlem64  39063  fourierdlem65  39064  fourierdlem95  39094  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  etransclem23  39150  etransclem35  39162  etransclem46  39173  fmtnorec2lem  39992  fmtnorec3  39998  pwdif  40039  m1expoddALTV  40099  perfectALTVlem2  40165  ztprmneprm  41918  altgsumbc  41923  divge1b  42096  divgt1b  42097