Theorem mulid2d 10924

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 10905	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  1c1 10803   · cmul 10807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-mulcom 10866  ax-mulass 10868  ax-distr 10869  ax-1rid 10872  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  adddirp1d  10932  addid1  11085  mulsubfacd  11366  mulcand  11538  receu  11550  divdivdiv  11606  divcan5  11607  subrec  11734  ltrec  11787  recp1lt1  11803  nndivtr  11950  subhalfhalf  12137  xp1d2m1eqxm1d2  12157  gtndiv  12327  lincmb01cmp  13156  iccf1o  13157  ltdifltdiv  13482  modfrac  13532  negmod  13564  addmodid  13567  m1expcl2  13732  expgt1  13749  ltexp2a  13812  leexp2a  13818  binom3  13867  faclbnd  13932  faclbnd4lem4  13938  facavg  13943  bcval5  13960  cshweqrep  14462  sqrlem2  14883  absimle  14949  reccn2  15234  iseraltlem2  15322  iseraltlem3  15323  o1fsum  15453  abscvgcvg  15459  ackbijnn  15468  binom1p  15471  binom1dif  15473  incexclem  15476  incexc  15477  climcndslem1  15489  pwdif  15508  geomulcvg  15516  fprodsplit  15604  fallrisefac  15663  bpolysum  15691  bpolydiflem  15692  bpoly4  15697  efcllem  15715  ef01bndlem  15821  efieq1re  15836  eirrlem  15841  iddvds  15907  pwp1fsum  16028  oddpwp1fsum  16029  bitsfzolem  16069  bitsfzo  16070  rpmulgcd  16194  prmind2  16318  isprm5  16340  phiprm  16406  eulerthlem2  16411  fermltl  16413  hashgcdlem  16417  odzdvds  16424  powm2modprm  16432  modprm0  16434  pythagtriplem4  16448  4sqlem18  16591  vdwapun  16603  mulgnnass  18653  odinv  19083  odadd2  19365  pgpfaclem2  19600  abvneg  20009  nrginvrcnlem  23761  nmoid  23812  blcvx  23867  icopnfcnv  24011  reparphti  24066  pcorevlem  24095  ncvsm1  24223  ncvspi  24225  cphipval2  24310  cphipval  24312  itg11  24760  itg2mulc  24817  itg2monolem1  24820  itgcnlem  24859  iblabs  24898  dvexp  25022  dvmptdiv  25043  dvef  25049  lhop1lem  25082  dvcvx  25089  dvfsumlem1  25095  dvfsumlem2  25096  dvfsumlem4  25098  dvfsum2  25103  plypow  25271  dgrcolem1  25339  vieta1lem2  25376  radcnvlem1  25477  radcnvlem2  25478  dvradcnv  25485  abelthlem6  25500  abelthlem7  25502  abelth2  25506  sinhalfpip  25554  sinhalfpim  25555  coshalfpip  25556  coshalfpim  25557  tangtx  25567  efif1olem4  25606  abslogle  25678  logdivlti  25680  advlog  25714  advlogexp  25715  logtayl  25720  cxpaddlelem  25809  cxpaddle  25810  affineequiv  25878  affineequiv2  25879  chordthmlem5  25891  dcubic2  25899  dcubic  25901  mcubic  25902  binom4  25905  dquartlem1  25906  quart1lem  25910  quart1  25911  quartlem1  25912  quart  25916  efiasin  25943  atantayl  25992  cvxcl  26039  scvxcvx  26040  lgamgulmlem5  26087  lgamcvg2  26109  lgam1  26118  wilthlem1  26122  wilthlem2  26123  basellem9  26143  fsumfldivdiaglem  26243  muinv  26247  chpub  26273  logexprlim  26278  mersenne  26280  perfectlem2  26283  dchrmulid2  26305  dchrptlem1  26317  dchrsum2  26321  sumdchr2  26323  bposlem2  26338  bposlem9  26345  lgsval2lem  26360  lgsval4a  26372  lgsneg1  26375  lgsdir2lem4  26381  lgsdir  26385  lgsmulsqcoprm  26396  lgsdirnn0  26397  lgsdinn0  26398  gausslemma2dlem1a  26418  gausslemma2dlem4  26422  gausslemma2dlem7  26426  gausslemma2d  26427  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem4  26431  lgsquad2lem1  26437  2sqlem8  26479  chebbnd1lem3  26524  chpchtlim  26532  rplogsumlem1  26537  rplogsumlem2  26538  rpvmasumlem  26540  dchrmusum2  26547  dchrvmasum2lem  26549  dchrvmasumlem2  26551  dchrvmasumlem3  26552  dchrisum0flblem1  26561  mulog2sumlem2  26588  vmalogdivsum2  26591  2vmadivsumlem  26593  log2sumbnd  26597  selberglem2  26599  selberg3lem1  26610  selberg4lem1  26613  pntrlog2bndlem2  26631  pntrlog2bndlem5  26634  pntpbnd1  26639  pntpbnd2  26640  pntibndlem2  26644  pntlemb  26650  pntlemr  26655  pntlemk  26659  pntlemo  26660  brbtwn2  27176  colinearalglem4  27180  ax5seglem3  27202  axbtwnid  27210  axpaschlem  27211  axeuclidlem  27233  axcontlem7  27241  axcontlem8  27242  elntg2  27256  nvm1  28928  nvpi  28930  nvmtri  28934  ipval2  28970  ipasslem1  29094  ipasslem4  29097  bcs2  29445  lnfnaddi  30306  nnmulge  30975  ccfldsrarelvec  31643  sqsscirc1  31760  indsum  31889  indsumin  31890  eulerpartlemgs2  32247  plymulx0  32426  logdivsqrle  32530  subfacp1lem6  33047  subfaclim  33050  cvxpconn  33104  cvxsconn  33105  resconn  33108  sinccvglem  33530  fwddifn0  34393  nn0prpwlem  34438  knoppndvlem9  34627  knoppndvlem14  34632  bj-bary1lem1  35409  mblfinlem3  35743  itg2addnclem3  35757  iblabsnc  35768  iblmulc2nc  35769  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  areacirclem1  35792  bfplem2  35908  bfp  35909  rrntotbnd  35921  lcmineqlem1  39965  lcmineqlem12  39976  lcmineqlem18  39982  aks4d1p1p7  40010  aks4d1p8  40023  fltnlta  40416  3cubeslem2  40423  3cubeslem3r  40425  irrapxlem5  40564  pellexlem2  40568  pellexlem6  40572  pellfundex  40624  jm2.19lem3  40729  jm2.25  40737  jm2.27c  40745  jm3.1lem2  40756  flcidc  40915  reabssgn  41133  sqrtcval  41138  int-mul12d  41683  cvgdvgrat  41820  bccn1  41851  binomcxplemnotnn0  41863  fperiodmullem  42732  xralrple2  42783  fmul01lt1lem2  43016  mccllem  43028  reclimc  43084  cosknegpi  43300  dvsinax  43344  dvnxpaek  43373  dvnmul  43374  itgsinexp  43386  stoweidlem14  43445  stoweidlem26  43457  wallispilem4  43499  wallispilem5  43500  wallispi2lem1  43502  wallispi2  43504  stirlinglem1  43505  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem10  43514  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkercncflem2  43535  fourierdlem26  43564  fourierdlem41  43579  fourierdlem42  43580  fourierdlem56  43593  fourierdlem57  43594  fourierdlem58  43595  fourierdlem62  43599  fourierdlem64  43601  fourierdlem65  43602  fourierdlem95  43632  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  etransclem23  43688  etransclem35  43700  etransclem46  43711  fmtnorec2lem  44882  fmtnorec3  44888  m1expoddALTV  44988  perfectALTVlem2  45062  ztprmneprm  45571  altgsumbc  45576  divge1b  45741  divgt1b  45742  ackval1  45915  affineid  45938  1subrec1sub  45939  rrx2vlinest  45975  line2x  45988