Theorem mullidi 11149

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   · cmul 11043

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  00id  11320  div4p1lem1div2  12408  3halfnz  12583  crreczi  14163  fac2  14214  hashxplem  14368  bpoly1  15986  bpoly2  15992  bpoly3  15993  bpoly4  15994  efival  16089  ef01bndlem  16121  3dvdsdec  16271  3dvds2dec  16272  odd2np1lem  16279  m1expo  16314  m1exp1  16315  nno  16321  divalglem5  16336  gcdaddmlem  16463  prmo2  16980  dec5nprm  17006  2exp8  17028  13prm  17055  23prm  17058  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  cnmsgnsubg  21544  sin2pim  26462  cos2pim  26463  sincosq3sgn  26477  sincosq4sgn  26478  tangtx  26482  sincosq1eq  26489  sincos4thpi  26490  sincos6thpi  26493  pige3ALT  26497  abssinper  26498  ang180lem2  26788  ang180lem3  26789  1cubr  26820  asin1  26872  dvatan  26913  log2cnv  26922  log2ublem3  26926  log2ub  26927  logfacbnd3  27202  bclbnd  27259  bpos1  27262  bposlem8  27270  lgsdilem  27303  lgsdir2lem1  27304  lgsdir2lem4  27307  lgsdir2lem5  27308  lgsdir2  27309  lgsdir  27311  2lgsoddprmlem3c  27391  dchrisum0flblem1  27487  rpvmasum2  27491  log2sumbnd  27523  ax5seglem7  29020  ex-fl  30534  ipasslem10  30926  hisubcomi  31191  normlem1  31197  normlem9  31205  norm-ii-i  31224  normsubi  31228  polid2i  31244  lnophmlem2  32104  lnfn0i  32129  nmopcoi  32182  unierri  32191  addltmulALT  32533  sgnmul  32926  dpmul4  33005  iconstr  33943  cos9thpiminplylem5  33963  logdivsqrle  34827  hgt750lem  34828  hgt750lem2  34829  problem4  35881  quad3  35883  cnndvlem1  36756  sin2h  37855  poimirlem26  37891  cntotbnd  38041  60gcd6e6  42368  12lcm5e60  42372  60lcm7e420  42374  3lexlogpow5ineq1  42418  3lexlogpow5ineq5  42424  sqdeccom12  42653  ex-decpmul  42670  1tiei  42681  sin2t3rdpi  42717  cos2t3rdpi  42718  areaquad  43567  resqrtvalex  43995  imsqrtvalex  43996  coskpi2  46218  stoweidlem13  46365  wallispilem2  46418  wallispilem4  46420  wallispi2lem1  46423  dirkerper  46448  dirkertrigeqlem1  46450  dirkercncflem1  46455  sqwvfoura  46580  sqwvfourb  46581  fourierswlem  46582  fouriersw  46583  lamberte  47242  rehalfge1  47689  257prm  47915  fmtnofac1  47924  fmtno4prmfac  47926  fmtno4nprmfac193  47928  fmtno5faclem1  47933  fmtno5faclem2  47934  139prmALT  47950  127prm  47953  11t31e341  48086  2exp340mod341  48087  nfermltl8rev  48096  tgoldbach  48171