Theorem mulid2i 10382

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mulid2i	⊢ (1 · 𝐴) = 𝐴

Proof of Theorem mulid2i

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mulid2 10375	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (1 · 𝐴) = 𝐴

Syntax hints:   = wceq 1601   ∈ wcel 2106  (class class class)co 6922  ℂcc 10270  1c1 10273   · cmul 10277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-mulcl 10334  ax-mulcom 10336  ax-mulass 10338  ax-distr 10339  ax-1rid 10342  ax-cnre 10345

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925

This theorem is referenced by:  00id  10551  halfpm6th  11603  div4p1lem1div2  11637  3halfnz  11808  crreczi  13308  fac2  13384  hashxplem  13534  bpoly1  15184  bpoly2  15190  bpoly3  15191  bpoly4  15192  efival  15284  ef01bndlem  15316  3dvdsdec  15460  3dvds2dec  15461  odd2np1lem  15468  m1expo  15505  m1exp1  15506  nno  15512  divalglem5  15527  gcdaddmlem  15651  prmo2  16148  dec5nprm  16174  2exp8  16195  13prm  16221  23prm  16224  37prm  16226  43prm  16227  83prm  16228  139prm  16229  163prm  16230  317prm  16231  631prm  16232  1259lem2  16237  1259lem3  16238  1259lem4  16239  1259lem5  16240  2503lem1  16242  2503lem2  16243  2503lem3  16244  2503prm  16245  4001lem1  16246  4001lem2  16247  4001lem3  16248  4001lem4  16249  cnmsgnsubg  20318  sin2pim  24675  cos2pim  24676  sincosq3sgn  24690  sincosq4sgn  24691  tangtx  24695  sincosq1eq  24702  sincos4thpi  24703  sincos6thpi  24705  pige3  24707  abssinper  24708  ang180lem2  24988  ang180lem3  24989  1cubr  25020  asin1  25072  dvatan  25113  log2cnv  25123  log2ublem3  25127  log2ub  25128  logfacbnd3  25400  bclbnd  25457  bpos1  25460  bposlem8  25468  lgsdilem  25501  lgsdir2lem1  25502  lgsdir2lem4  25505  lgsdir2lem5  25506  lgsdir2  25507  lgsdir  25509  2lgsoddprmlem3c  25589  dchrisum0flblem1  25649  rpvmasum2  25653  log2sumbnd  25685  ax5seglem7  26284  ex-fl  27879  ipasslem10  28266  hisubcomi  28533  normlem1  28539  normlem9  28547  norm-ii-i  28566  normsubi  28570  polid2i  28586  lnophmlem2  29448  lnfn0i  29473  nmopcoi  29526  unierri  29535  addltmulALT  29877  dpmul4  30184  sgnmul  31203  logdivsqrle  31330  hgt750lem  31331  hgt750lem2  31332  problem4  32159  quad3  32161  cnndvlem1  33110  sin2h  34008  poimirlem26  34045  cntotbnd  34203  sqdeccom12  38137  ex-decpmul  38140  areaquad  38742  coskpi2  40987  stoweidlem13  41139  wallispilem2  41192  wallispilem4  41194  wallispi2lem1  41197  dirkerper  41222  dirkertrigeqlem1  41224  dirkercncflem1  41229  sqwvfoura  41354  sqwvfourb  41355  fourierswlem  41356  fouriersw  41357  257prm  42476  fmtnofac1  42485  fmtno4prmfac  42487  fmtno4nprmfac193  42489  fmtno5faclem1  42494  fmtno5faclem2  42495  139prmALT  42514  127prm  42518  tgoldbach  42712