Theorem mullidi 11137

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   · cmul 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-mulcom 11090  ax-mulass 11092  ax-distr 11093  ax-1rid 11096  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  00id  11308  div4p1lem1div2  12396  3halfnz  12571  crreczi  14151  fac2  14202  hashxplem  14356  bpoly1  15974  bpoly2  15980  bpoly3  15981  bpoly4  15982  efival  16077  ef01bndlem  16109  3dvdsdec  16259  3dvds2dec  16260  odd2np1lem  16267  m1expo  16302  m1exp1  16303  nno  16309  divalglem5  16324  gcdaddmlem  16451  prmo2  16968  dec5nprm  16994  2exp8  17016  13prm  17043  23prm  17046  37prm  17048  43prm  17049  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  cnmsgnsubg  21532  sin2pim  26450  cos2pim  26451  sincosq3sgn  26465  sincosq4sgn  26466  tangtx  26470  sincosq1eq  26477  sincos4thpi  26478  sincos6thpi  26481  pige3ALT  26485  abssinper  26486  ang180lem2  26776  ang180lem3  26777  1cubr  26808  asin1  26860  dvatan  26901  log2cnv  26910  log2ublem3  26914  log2ub  26915  logfacbnd3  27190  bclbnd  27247  bpos1  27250  bposlem8  27258  lgsdilem  27291  lgsdir2lem1  27292  lgsdir2lem4  27295  lgsdir2lem5  27296  lgsdir2  27297  lgsdir  27299  2lgsoddprmlem3c  27379  dchrisum0flblem1  27475  rpvmasum2  27479  log2sumbnd  27511  ax5seglem7  29008  ex-fl  30522  ipasslem10  30914  hisubcomi  31179  normlem1  31185  normlem9  31193  norm-ii-i  31212  normsubi  31216  polid2i  31232  lnophmlem2  32092  lnfn0i  32117  nmopcoi  32170  unierri  32179  addltmulALT  32521  sgnmul  32916  dpmul4  32995  iconstr  33923  cos9thpiminplylem5  33943  logdivsqrle  34807  hgt750lem  34808  hgt750lem2  34809  problem4  35862  quad3  35864  cnndvlem1  36737  sin2h  37807  poimirlem26  37843  cntotbnd  37993  60gcd6e6  42254  12lcm5e60  42258  60lcm7e420  42260  3lexlogpow5ineq1  42304  3lexlogpow5ineq5  42310  sqdeccom12  42540  ex-decpmul  42557  1tiei  42568  sin2t3rdpi  42604  cos2t3rdpi  42605  areaquad  43454  resqrtvalex  43882  imsqrtvalex  43883  coskpi2  46106  stoweidlem13  46253  wallispilem2  46306  wallispilem4  46308  wallispi2lem1  46311  dirkerper  46336  dirkertrigeqlem1  46338  dirkercncflem1  46343  sqwvfoura  46468  sqwvfourb  46469  fourierswlem  46470  fouriersw  46471  lamberte  47130  rehalfge1  47577  257prm  47803  fmtnofac1  47812  fmtno4prmfac  47814  fmtno4nprmfac193  47816  fmtno5faclem1  47821  fmtno5faclem2  47822  139prmALT  47838  127prm  47841  11t31e341  47974  2exp340mod341  47975  nfermltl8rev  47984  tgoldbach  48059