Theorem mullidi 11202

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

Syntax hints:   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086  1c1 11089   · cmul 11093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-mulcl 11150  ax-mulcom 11152  ax-mulass 11154  ax-distr 11155  ax-1rid 11158  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403

This theorem is referenced by:  00id  11373  div4p1lem1div2  12490  3halfnz  12666  crreczi  14255  fac2  14306  hashxplem  14460  sgnmul  15134  bpoly1  16095  bpoly2  16101  bpoly3  16102  bpoly4  16103  efival  16198  ef01bndlem  16230  3dvdsdec  16380  3dvds2dec  16381  odd2np1lem  16388  m1expo  16423  m1exp1  16424  nno  16430  divalglem5  16445  gcdaddmlem  16572  prmo2  17090  dec5nprm  17116  2exp8  17138  13prm  17166  23prm  17169  37prm  17171  43prm  17172  83prm  17173  139prm  17174  163prm  17175  317prm  17176  631prm  17177  1259lem2  17182  1259lem3  17183  1259lem4  17184  1259lem5  17185  2503lem1  17187  2503lem2  17188  2503lem3  17189  2503prm  17190  4001lem1  17191  4001lem2  17192  4001lem3  17193  4001lem4  17194  cnmsgnsubg  21687  sin2pim  26608  cos2pim  26609  sincosq3sgn  26623  sincosq4sgn  26624  tangtx  26628  sincosq1eq  26635  sincos4thpi  26636  sincos6thpi  26639  pige3ALT  26643  abssinper  26644  ang180lem2  26933  ang180lem3  26934  1cubr  26965  asin1  27017  dvatan  27058  log2cnv  27067  log2ublem3  27071  log2ub  27072  logfacbnd3  27345  bclbnd  27402  bpos1  27405  bposlem8  27413  lgsdilem  27446  lgsdir2lem1  27447  lgsdir2lem4  27450  lgsdir2lem5  27451  lgsdir2  27452  lgsdir  27454  2lgsoddprmlem3c  27534  dchrisum0flblem1  27630  rpvmasum2  27634  log2sumbnd  27666  ax5seglem7  29194  ex-fl  30707  ipasslem10  31100  hisubcomi  31365  normlem1  31371  normlem9  31379  norm-ii-i  31398  normsubi  31402  polid2i  31418  lnophmlem2  32278  lnfn0i  32303  nmopcoi  32356  unierri  32365  addltmulALT  32707  dpmul4  33146  iconstr  34073  cos9thpiminplylem5  34093  logdivsqrle  34954  hgt750lem  34955  hgt750lem2  34956  problem4  36031  quad3  36033  cnndvlem1  36988  sin2h  38121  poimirlem26  38157  cntotbnd  38307  60gcd6e6  42633  12lcm5e60  42637  60lcm7e420  42639  3lexlogpow5ineq1  42683  3lexlogpow5ineq5  42689  sqdeccom12  42910  ex-decpmul  42927  1tiei  42938  sin2t3rdpi  42974  cos2t3rdpi  42975  areaquad  43805  resqrtvalex  44233  imsqrtvalex  44234  coskpi2  46438  stoweidlem13  46585  wallispilem2  46638  wallispilem4  46640  wallispi2lem1  46643  dirkerper  46668  dirkertrigeqlem1  46670  dirkercncflem1  46675  sqwvfoura  46800  sqwvfourb  46801  fourierswlem  46802  fouriersw  46803  cos5t  47471  lamberte  47480  rehalfge1  47931  257prm  48168  fmtnofac1  48177  fmtno4prmfac  48179  fmtno4nprmfac193  48181  fmtno5faclem1  48186  fmtno5faclem2  48187  139prmALT  48203  127prm  48206  11t31e341  48352  2exp340mod341  48353  nfermltl8rev  48362  tgoldbach  48437