Theorem mulid2 10958

Description: Identity law for multiplication. See mulid1 10957 for commuted version. (Contributed by NM, 8-Oct-1999.)

Assertion

Ref	Expression
mulid2	⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Proof of Theorem mulid2

Step	Hyp	Ref	Expression
1		ax-1cn 10913	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 10941	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 686	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulid1 10957	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2779	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853  1c1 10856   · cmul 10860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-resscn 10912  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-mulcl 10917  ax-mulcom 10919  ax-mulass 10921  ax-distr 10922  ax-1rid 10925  ax-cnre 10928

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271

This theorem is referenced by:  mulid2i  10964  mulid2d  10977  muladd11  11128  1p1times  11129  mul02lem1  11134  cnegex2  11140  mulm1  11399  div1  11647  subdivcomb2  11654  recdiv  11664  divdiv2  11670  conjmul  11675  ser1const  13760  expp1  13770  recan  15029  arisum  15553  geo2sum  15566  prodrblem  15620  prodmolem2a  15625  risefac1  15724  fallfac1  15725  bpoly3  15749  bpoly4  15750  sinhval  15844  coshval  15845  demoivreALT  15891  gcdadd  16214  gcdid  16215  cncrng  20600  cnfld1  20604  blcvx  23942  icccvx  24094  cnlmod  24284  coeidp  25405  dgrid  25406  quartlem1  25988  asinsinlem  26022  asinsin  26023  atantan  26054  musumsum  26322  brbtwn2  27254  axsegconlem1  27266  ax5seglem1  27277  ax5seglem2  27278  ax5seglem4  27281  ax5seglem5  27282  axeuclid  27312  axcontlem2  27314  axcontlem4  27316  cncvcOLD  28924  dvcosax  43421