Theorem mullidi 11317

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201  1c1 11204   · cmul 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-mulcl 11265  ax-mulcom 11267  ax-mulass 11269  ax-distr 11270  ax-1rid 11273  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  00id  11488  div4p1lem1div2  12604  3halfnz  12781  crreczi  14375  fac2  14426  hashxplem  14581  sgnmul  15265  bpoly1  16222  bpoly2  16228  bpoly3  16229  bpoly4  16230  efival  16325  ef01bndlem  16357  3dvdsdec  16507  3dvds2dec  16508  odd2np1lem  16515  m1expo  16550  m1exp1  16551  nno  16557  divalglem5  16572  gcdaddmlem  16701  prmo2  17223  dec5nprm  17249  2exp8  17271  13prm  17299  23prm  17302  37prm  17304  43prm  17305  83prm  17306  139prm  17307  163prm  17308  317prm  17309  631prm  17310  1259lem2  17315  1259lem3  17316  1259lem4  17317  1259lem5  17318  2503lem1  17320  2503lem2  17321  2503lem3  17322  2503prm  17323  4001lem1  17324  4001lem2  17325  4001lem3  17326  4001lem4  17327  cnmsgnsubg  21888  iaa  26656  sin2pim  26819  cos2pim  26820  sincosq3sgn  26834  sincosq4sgn  26835  tangtx  26839  sincosq1eq  26846  sincos4thpi  26847  sincos6thpi  26849  pige3ALT  26853  abssinper  26854  ang180lem2  27143  ang180lem3  27144  1cubr  27175  asin1  27227  dvatan  27268  log2cnv  27277  log2ublem3  27281  log2ub  27282  logfacbnd3  27555  bclbnd  27612  bpos1  27615  bposlem8  27623  lgsdilem  27656  lgsdir2lem1  27657  lgsdir2lem4  27660  lgsdir2lem5  27661  lgsdir2  27662  lgsdir  27664  2lgsoddprmlem3c  27744  dchrisum0flblem1  27840  rpvmasum2  27844  log2sumbnd  27876  ax5seglem7  29518  ex-fl  31053  ipasslem10  31446  hisubcomi  31711  normlem1  31717  normlem9  31725  norm-ii-i  31744  normsubi  31748  polid2i  31764  lnophmlem2  32624  lnfn0i  32649  nmopcoi  32702  unierri  32711  addltmulALT  33095  dpmul4  33526  iconstr  34444  cos9thpiminplylem5  34464  logdivsqrle  35325  hgt750lem  35326  hgt750lem2  35327  problem4  36519  quad3  36521  cnndvlem1  37495  sin2h  38626  poimirlem26  38657  cntotbnd  38823  60gcd6e6  43147  12lcm5e60  43151  60lcm7e420  43153  3lexlogpow5ineq1  43197  3lexlogpow5ineq5  43203  sqdeccom12  43439  ex-decpmul  43456  1tiei  43467  sin2t3rdpi  43497  cos2t3rdpi  43498  areaquad  44311  resqrtvalex  44738  imsqrtvalex  44739  coskpi2  46969  stoweidlem13  47116  wallispilem2  47169  wallispilem4  47171  wallispi2lem1  47174  dirkerper  47199  dirkertrigeqlem1  47201  dirkercncflem1  47206  sqwvfoura  47331  sqwvfourb  47332  fourierswlem  47333  fouriersw  47334  cos5t  48018  goldpolyfactor  48020  goldratval  48029  lamberte  48031  rehalfge1  48502  257prm  48739  fmtnofac1  48748  fmtno4prmfac  48750  fmtno4nprmfac193  48752  fmtno5faclem1  48757  fmtno5faclem2  48758  139prmALT  48774  127prm  48777  11t31e341  48923  2exp340mod341  48924  nfermltl8rev  48933  tgoldbach  49008