Theorem mullidi 11150

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 7367  ℂ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 2708  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 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  00id  11321  div4p1lem1div2  12432  3halfnz  12608  crreczi  14190  fac2  14241  hashxplem  14395  bpoly1  16016  bpoly2  16022  bpoly3  16023  bpoly4  16024  efival  16119  ef01bndlem  16151  3dvdsdec  16301  3dvds2dec  16302  odd2np1lem  16309  m1expo  16344  m1exp1  16345  nno  16351  divalglem5  16366  gcdaddmlem  16493  prmo2  17011  dec5nprm  17037  2exp8  17059  13prm  17086  23prm  17089  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  cnmsgnsubg  21557  sin2pim  26449  cos2pim  26450  sincosq3sgn  26464  sincosq4sgn  26465  tangtx  26469  sincosq1eq  26476  sincos4thpi  26477  sincos6thpi  26480  pige3ALT  26484  abssinper  26485  ang180lem2  26774  ang180lem3  26775  1cubr  26806  asin1  26858  dvatan  26899  log2cnv  26908  log2ublem3  26912  log2ub  26913  logfacbnd3  27186  bclbnd  27243  bpos1  27246  bposlem8  27254  lgsdilem  27287  lgsdir2lem1  27288  lgsdir2lem4  27291  lgsdir2lem5  27292  lgsdir2  27293  lgsdir  27295  2lgsoddprmlem3c  27375  dchrisum0flblem1  27471  rpvmasum2  27475  log2sumbnd  27507  ax5seglem7  29004  ex-fl  30517  ipasslem10  30910  hisubcomi  31175  normlem1  31181  normlem9  31189  norm-ii-i  31208  normsubi  31212  polid2i  31228  lnophmlem2  32088  lnfn0i  32113  nmopcoi  32166  unierri  32175  addltmulALT  32517  sgnmul  32908  dpmul4  32973  iconstr  33910  cos9thpiminplylem5  33930  logdivsqrle  34794  hgt750lem  34795  hgt750lem2  34796  problem4  35850  quad3  35852  cnndvlem1  36797  sin2h  37931  poimirlem26  37967  cntotbnd  38117  60gcd6e6  42443  12lcm5e60  42447  60lcm7e420  42449  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  sqdeccom12  42721  ex-decpmul  42738  1tiei  42749  sin2t3rdpi  42785  cos2t3rdpi  42786  areaquad  43644  resqrtvalex  44072  imsqrtvalex  44073  coskpi2  46294  stoweidlem13  46441  wallispilem2  46494  wallispilem4  46496  wallispi2lem1  46499  dirkerper  46524  dirkertrigeqlem1  46526  dirkercncflem1  46531  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  cos5t  47327  lamberte  47336  rehalfge1  47787  257prm  48024  fmtnofac1  48033  fmtno4prmfac  48035  fmtno4nprmfac193  48037  fmtno5faclem1  48042  fmtno5faclem2  48043  139prmALT  48059  127prm  48062  11t31e341  48208  2exp340mod341  48209  nfermltl8rev  48218  tgoldbach  48293