Theorem mullidi 11124

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011  1c1 11014   · cmul 11018

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 2705  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-mulcl 11075  ax-mulcom 11077  ax-mulass 11079  ax-distr 11080  ax-1rid 11083  ax-cnre 11086

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 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355

This theorem is referenced by:  00id  11295  div4p1lem1div2  12383  3halfnz  12558  crreczi  14137  fac2  14188  hashxplem  14342  bpoly1  15960  bpoly2  15966  bpoly3  15967  bpoly4  15968  efival  16063  ef01bndlem  16095  3dvdsdec  16245  3dvds2dec  16246  odd2np1lem  16253  m1expo  16288  m1exp1  16289  nno  16295  divalglem5  16310  gcdaddmlem  16437  prmo2  16954  dec5nprm  16980  2exp8  17002  13prm  17029  23prm  17032  37prm  17034  43prm  17035  83prm  17036  139prm  17037  163prm  17038  317prm  17039  631prm  17040  1259lem2  17045  1259lem3  17046  1259lem4  17047  1259lem5  17048  2503lem1  17050  2503lem2  17051  2503lem3  17052  2503prm  17053  4001lem1  17054  4001lem2  17055  4001lem3  17056  4001lem4  17057  cnmsgnsubg  21516  sin2pim  26422  cos2pim  26423  sincosq3sgn  26437  sincosq4sgn  26438  tangtx  26442  sincosq1eq  26449  sincos4thpi  26450  sincos6thpi  26453  pige3ALT  26457  abssinper  26458  ang180lem2  26748  ang180lem3  26749  1cubr  26780  asin1  26832  dvatan  26873  log2cnv  26882  log2ublem3  26886  log2ub  26887  logfacbnd3  27162  bclbnd  27219  bpos1  27222  bposlem8  27230  lgsdilem  27263  lgsdir2lem1  27264  lgsdir2lem4  27267  lgsdir2lem5  27268  lgsdir2  27269  lgsdir  27271  2lgsoddprmlem3c  27351  dchrisum0flblem1  27447  rpvmasum2  27451  log2sumbnd  27483  ax5seglem7  28915  ex-fl  30429  ipasslem10  30821  hisubcomi  31086  normlem1  31092  normlem9  31100  norm-ii-i  31119  normsubi  31123  polid2i  31139  lnophmlem2  31999  lnfn0i  32024  nmopcoi  32077  unierri  32086  addltmulALT  32428  sgnmul  32823  dpmul4  32901  iconstr  33800  cos9thpiminplylem5  33820  logdivsqrle  34684  hgt750lem  34685  hgt750lem2  34686  problem4  35733  quad3  35735  cnndvlem1  36602  sin2h  37671  poimirlem26  37707  cntotbnd  37857  60gcd6e6  42118  12lcm5e60  42122  60lcm7e420  42124  3lexlogpow5ineq1  42168  3lexlogpow5ineq5  42174  sqdeccom12  42408  ex-decpmul  42425  1tiei  42436  sin2t3rdpi  42472  cos2t3rdpi  42473  areaquad  43334  resqrtvalex  43763  imsqrtvalex  43764  coskpi2  45989  stoweidlem13  46136  wallispilem2  46189  wallispilem4  46191  wallispi2lem1  46194  dirkerper  46219  dirkertrigeqlem1  46221  dirkercncflem1  46226  sqwvfoura  46351  sqwvfourb  46352  fourierswlem  46353  fouriersw  46354  lamberte  47013  rehalfge1  47460  257prm  47686  fmtnofac1  47695  fmtno4prmfac  47697  fmtno4nprmfac193  47699  fmtno5faclem1  47704  fmtno5faclem2  47705  139prmALT  47721  127prm  47724  11t31e341  47857  2exp340mod341  47858  nfermltl8rev  47867  tgoldbach  47942