Theorem mullidi 11218

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mullidi	⊢ (1 · 𝐴) = 𝐴

Proof of Theorem mullidi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mullid 11212	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (1 · 𝐴) = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107  1c1 11110   · cmul 11114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-mulcl 11171  ax-mulcom 11173  ax-mulass 11175  ax-distr 11176  ax-1rid 11179  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7411

This theorem is referenced by:  00id  11388  halfpm6th  12432  div4p1lem1div2  12466  3halfnz  12640  crreczi  14190  fac2  14238  hashxplem  14392  bpoly1  15994  bpoly2  16000  bpoly3  16001  bpoly4  16002  efival  16094  ef01bndlem  16126  3dvdsdec  16274  3dvds2dec  16275  odd2np1lem  16282  m1expo  16317  m1exp1  16318  nno  16324  divalglem5  16339  gcdaddmlem  16464  prmo2  16972  dec5nprm  16998  2exp8  17021  13prm  17048  23prm  17051  37prm  17053  43prm  17054  83prm  17055  139prm  17056  163prm  17057  317prm  17058  631prm  17059  1259lem2  17064  1259lem3  17065  1259lem4  17066  1259lem5  17067  2503lem1  17069  2503lem2  17070  2503lem3  17071  2503prm  17072  4001lem1  17073  4001lem2  17074  4001lem3  17075  4001lem4  17076  cnmsgnsubg  21129  sin2pim  25994  cos2pim  25995  sincosq3sgn  26009  sincosq4sgn  26010  tangtx  26014  sincosq1eq  26021  sincos4thpi  26022  sincos6thpi  26024  pige3ALT  26028  abssinper  26029  ang180lem2  26312  ang180lem3  26313  1cubr  26344  asin1  26396  dvatan  26437  log2cnv  26446  log2ublem3  26450  log2ub  26451  logfacbnd3  26723  bclbnd  26780  bpos1  26783  bposlem8  26791  lgsdilem  26824  lgsdir2lem1  26825  lgsdir2lem4  26828  lgsdir2lem5  26829  lgsdir2  26830  lgsdir  26832  2lgsoddprmlem3c  26912  dchrisum0flblem1  27008  rpvmasum2  27012  log2sumbnd  27044  ax5seglem7  28190  ex-fl  29697  ipasslem10  30087  hisubcomi  30352  normlem1  30358  normlem9  30366  norm-ii-i  30385  normsubi  30389  polid2i  30405  lnophmlem2  31265  lnfn0i  31290  nmopcoi  31343  unierri  31352  addltmulALT  31694  dpmul4  32075  sgnmul  33536  logdivsqrle  33657  hgt750lem  33658  hgt750lem2  33659  problem4  34648  quad3  34650  cnndvlem1  35408  sin2h  36473  poimirlem26  36509  cntotbnd  36659  60gcd6e6  40864  12lcm5e60  40868  60lcm7e420  40870  3lexlogpow5ineq1  40914  3lexlogpow5ineq5  40920  sqdeccom12  41203  ex-decpmul  41206  areaquad  41955  resqrtvalex  42386  imsqrtvalex  42387  coskpi2  44572  stoweidlem13  44719  wallispilem2  44772  wallispilem4  44774  wallispi2lem1  44777  dirkerper  44802  dirkertrigeqlem1  44804  dirkercncflem1  44809  sqwvfoura  44934  sqwvfourb  44935  fourierswlem  44936  fouriersw  44937  257prm  46219  fmtnofac1  46228  fmtno4prmfac  46230  fmtno4nprmfac193  46232  fmtno5faclem1  46237  fmtno5faclem2  46238  139prmALT  46254  127prm  46257  11t31e341  46390  2exp340mod341  46391  nfermltl8rev  46400  tgoldbach  46475