Theorem mullidi 11238

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125  1c1 11128   · cmul 11132

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  00id  11408  div4p1lem1div2  12494  3halfnz  12670  crreczi  14244  fac2  14295  hashxplem  14449  bpoly1  16065  bpoly2  16071  bpoly3  16072  bpoly4  16073  efival  16168  ef01bndlem  16200  3dvdsdec  16349  3dvds2dec  16350  odd2np1lem  16357  m1expo  16392  m1exp1  16393  nno  16399  divalglem5  16414  gcdaddmlem  16541  prmo2  17058  dec5nprm  17084  2exp8  17106  13prm  17133  23prm  17136  37prm  17138  43prm  17139  83prm  17140  139prm  17141  163prm  17142  317prm  17143  631prm  17144  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  2503lem1  17154  2503lem2  17155  2503lem3  17156  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem3  17160  4001lem4  17161  cnmsgnsubg  21535  sin2pim  26444  cos2pim  26445  sincosq3sgn  26459  sincosq4sgn  26460  tangtx  26464  sincosq1eq  26471  sincos4thpi  26472  sincos6thpi  26475  pige3ALT  26479  abssinper  26480  ang180lem2  26770  ang180lem3  26771  1cubr  26802  asin1  26854  dvatan  26895  log2cnv  26904  log2ublem3  26908  log2ub  26909  logfacbnd3  27184  bclbnd  27241  bpos1  27244  bposlem8  27252  lgsdilem  27285  lgsdir2lem1  27286  lgsdir2lem4  27289  lgsdir2lem5  27290  lgsdir2  27291  lgsdir  27293  2lgsoddprmlem3c  27373  dchrisum0flblem1  27469  rpvmasum2  27473  log2sumbnd  27505  ax5seglem7  28860  ex-fl  30374  ipasslem10  30766  hisubcomi  31031  normlem1  31037  normlem9  31045  norm-ii-i  31064  normsubi  31068  polid2i  31084  lnophmlem2  31944  lnfn0i  31969  nmopcoi  32022  unierri  32031  addltmulALT  32373  sgnmul  32760  dpmul4  32834  iconstr  33746  cos9thpiminplylem5  33766  logdivsqrle  34628  hgt750lem  34629  hgt750lem2  34630  problem4  35636  quad3  35638  cnndvlem1  36501  sin2h  37580  poimirlem26  37616  cntotbnd  37766  60gcd6e6  41963  12lcm5e60  41967  60lcm7e420  41969  3lexlogpow5ineq1  42013  3lexlogpow5ineq5  42019  sqdeccom12  42286  ex-decpmul  42302  1tiei  42313  areaquad  43187  resqrtvalex  43616  imsqrtvalex  43617  coskpi2  45843  stoweidlem13  45990  wallispilem2  46043  wallispilem4  46045  wallispi2lem1  46048  dirkerper  46073  dirkertrigeqlem1  46075  dirkercncflem1  46080  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  lamberte  46868  rehalfge1  47312  257prm  47523  fmtnofac1  47532  fmtno4prmfac  47534  fmtno4nprmfac193  47536  fmtno5faclem1  47541  fmtno5faclem2  47542  139prmALT  47558  127prm  47561  11t31e341  47694  2exp340mod341  47695  nfermltl8rev  47704  tgoldbach  47779