Theorem mullid 11212

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

Assertion

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

Proof of Theorem mullid

Step	Hyp	Ref	Expression
1		ax-1cn 11167	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11195	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 688	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11211	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2772	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107  1c1 11110   · cmul 11114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-mulcl 11171  ax-mulcom 11173  ax-mulass 11175  ax-distr 11176  ax-1rid 11179  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7411

This theorem is referenced by:  mullidi  11218  mullidd  11231  muladd11  11383  1p1times  11384  mul02lem1  11389  cnegex2  11395  mulm1  11654  div1  11902  subdivcomb2  11909  recdiv  11919  divdiv2  11925  conjmul  11930  ser1const  14023  expp1  14033  recan  15282  arisum  15805  geo2sum  15818  prodrblem  15872  prodmolem2a  15877  risefac1  15976  fallfac1  15977  bpoly3  16001  bpoly4  16002  sinhval  16096  coshval  16097  demoivreALT  16143  gcdadd  16466  gcdid  16467  cncrng  20965  cnfld1  20969  blcvx  24313  icccvx  24465  cnlmod  24655  coeidp  25776  dgrid  25777  quartlem1  26359  asinsinlem  26393  asinsin  26394  atantan  26425  musumsum  26693  brbtwn2  28160  axsegconlem1  28172  ax5seglem1  28183  ax5seglem2  28184  ax5seglem4  28187  ax5seglem5  28188  axeuclid  28218  axcontlem2  28220  axcontlem4  28222  cncvcOLD  29831  dvcosax  44632