Theorem mullidi 11179

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   · cmul 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  00id  11349  div4p1lem1div2  12437  3halfnz  12613  crreczi  14193  fac2  14244  hashxplem  14398  bpoly1  16017  bpoly2  16023  bpoly3  16024  bpoly4  16025  efival  16120  ef01bndlem  16152  3dvdsdec  16302  3dvds2dec  16303  odd2np1lem  16310  m1expo  16345  m1exp1  16346  nno  16352  divalglem5  16367  gcdaddmlem  16494  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  21486  sin2pim  26394  cos2pim  26395  sincosq3sgn  26409  sincosq4sgn  26410  tangtx  26414  sincosq1eq  26421  sincos4thpi  26422  sincos6thpi  26425  pige3ALT  26429  abssinper  26430  ang180lem2  26720  ang180lem3  26721  1cubr  26752  asin1  26804  dvatan  26845  log2cnv  26854  log2ublem3  26858  log2ub  26859  logfacbnd3  27134  bclbnd  27191  bpos1  27194  bposlem8  27202  lgsdilem  27235  lgsdir2lem1  27236  lgsdir2lem4  27239  lgsdir2lem5  27240  lgsdir2  27241  lgsdir  27243  2lgsoddprmlem3c  27323  dchrisum0flblem1  27419  rpvmasum2  27423  log2sumbnd  27455  ax5seglem7  28862  ex-fl  30376  ipasslem10  30768  hisubcomi  31033  normlem1  31039  normlem9  31047  norm-ii-i  31066  normsubi  31070  polid2i  31086  lnophmlem2  31946  lnfn0i  31971  nmopcoi  32024  unierri  32033  addltmulALT  32375  sgnmul  32760  dpmul4  32834  iconstr  33756  cos9thpiminplylem5  33776  logdivsqrle  34641  hgt750lem  34642  hgt750lem2  34643  problem4  35655  quad3  35657  cnndvlem1  36525  sin2h  37604  poimirlem26  37640  cntotbnd  37790  60gcd6e6  41992  12lcm5e60  41996  60lcm7e420  41998  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  sqdeccom12  42277  ex-decpmul  42294  1tiei  42305  sin2t3rdpi  42341  cos2t3rdpi  42342  areaquad  43205  resqrtvalex  43634  imsqrtvalex  43635  coskpi2  45864  stoweidlem13  46011  wallispilem2  46064  wallispilem4  46066  wallispi2lem1  46069  dirkerper  46094  dirkertrigeqlem1  46096  dirkercncflem1  46101  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  lamberte  46889  rehalfge1  47336  257prm  47562  fmtnofac1  47571  fmtno4prmfac  47573  fmtno4nprmfac193  47575  fmtno5faclem1  47580  fmtno5faclem2  47581  139prmALT  47597  127prm  47600  11t31e341  47733  2exp340mod341  47734  nfermltl8rev  47743  tgoldbach  47818