Theorem mullidi 11232

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 11225	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (1 · 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116  1c1 11119   · cmul 11123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-mulcl 11180  ax-mulcom 11182  ax-mulass 11184  ax-distr 11185  ax-1rid 11188  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  00id  11403  div4p1lem1div2  12517  3halfnz  12693  crreczi  14284  fac2  14335  hashxplem  14490  sgnmul  15170  bpoly1  16130  bpoly2  16136  bpoly3  16137  bpoly4  16138  efival  16233  ef01bndlem  16265  3dvdsdec  16415  3dvds2dec  16416  odd2np1lem  16423  m1expo  16458  m1exp1  16459  nno  16465  divalglem5  16480  gcdaddmlem  16607  prmo2  17125  dec5nprm  17151  2exp8  17173  13prm  17201  23prm  17204  37prm  17206  43prm  17207  83prm  17208  139prm  17209  163prm  17210  317prm  17211  631prm  17212  1259lem2  17217  1259lem3  17218  1259lem4  17219  1259lem5  17220  2503lem1  17222  2503lem2  17223  2503lem3  17224  2503prm  17225  4001lem1  17226  4001lem2  17227  4001lem3  17228  4001lem4  17229  cnmsgnsubg  21764  sin2pim  26687  cos2pim  26688  sincosq3sgn  26702  sincosq4sgn  26703  tangtx  26707  sincosq1eq  26714  sincos4thpi  26715  sincos6thpi  26718  pige3ALT  26722  abssinper  26723  ang180lem2  27012  ang180lem3  27013  1cubr  27044  asin1  27096  dvatan  27137  log2cnv  27146  log2ublem3  27150  log2ub  27151  logfacbnd3  27424  bclbnd  27481  bpos1  27484  bposlem8  27492  lgsdilem  27525  lgsdir2lem1  27526  lgsdir2lem4  27529  lgsdir2lem5  27530  lgsdir2  27531  lgsdir  27533  2lgsoddprmlem3c  27613  dchrisum0flblem1  27709  rpvmasum2  27713  log2sumbnd  27745  ax5seglem7  29322  ex-fl  30835  ipasslem10  31228  hisubcomi  31493  normlem1  31499  normlem9  31507  norm-ii-i  31526  normsubi  31530  polid2i  31546  lnophmlem2  32406  lnfn0i  32431  nmopcoi  32484  unierri  32493  addltmulALT  32835  dpmul4  33270  iconstr  34187  cos9thpiminplylem5  34207  logdivsqrle  35069  hgt750lem  35070  hgt750lem2  35071  problem4  36181  quad3  36183  cnndvlem1  37167  sin2h  38302  poimirlem26  38338  cntotbnd  38488  60gcd6e6  42812  12lcm5e60  42816  60lcm7e420  42818  3lexlogpow5ineq1  42862  3lexlogpow5ineq5  42868  sqdeccom12  43091  ex-decpmul  43108  1tiei  43119  sin2t3rdpi  43155  cos2t3rdpi  43156  areaquad  43984  resqrtvalex  44412  imsqrtvalex  44413  coskpi2  46621  stoweidlem13  46768  wallispilem2  46821  wallispilem4  46823  wallispi2lem1  46826  dirkerper  46851  dirkertrigeqlem1  46853  dirkercncflem1  46858  sqwvfoura  46983  sqwvfourb  46984  fourierswlem  46985  fouriersw  46986  cos5t  47657  lamberte  47666  rehalfge1  48117  257prm  48354  fmtnofac1  48363  fmtno4prmfac  48365  fmtno4nprmfac193  48367  fmtno5faclem1  48372  fmtno5faclem2  48373  139prmALT  48389  127prm  48392  11t31e341  48538  2exp340mod341  48539  nfermltl8rev  48548  tgoldbach  48623