Theorem mullid 11132

Description: Identity law for multiplication. See mulrid 11131 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 11085	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11113	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 691	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11131	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2772	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025  1c1 11028   · cmul 11032

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-mulcl 11089  ax-mulcom 11091  ax-mulass 11093  ax-distr 11094  ax-1rid 11097  ax-cnre 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361

This theorem is referenced by:  mullidi  11139  mullidd  11152  muladd11  11305  1p1times  11306  mul02lem1  11311  cnegex2  11317  mulm1  11580  div1  11833  subdivcomb2  11840  recdiv  11850  divdiv2  11856  conjmul  11861  ser1const  14009  expp1  14019  recan  15288  arisum  15814  geo2sum  15827  prodrblem  15883  prodmolem2a  15888  risefac1  15987  fallfac1  15988  bpoly3  16012  bpoly4  16013  sinhval  16110  coshval  16111  demoivreALT  16157  gcdadd  16484  gcdid  16485  cncrng  21376  cncrngOLD  21377  cnfld1  21381  cnfld1OLD  21382  blcvx  24772  icccvx  24926  cnlmod  25116  coeidp  26240  dgrid  26241  quartlem1  26838  asinsinlem  26872  asinsin  26873  atantan  26904  musumsum  27173  brbtwn2  28993  axsegconlem1  29005  ax5seglem1  29016  ax5seglem2  29017  ax5seglem4  29020  ax5seglem5  29021  axeuclid  29051  axcontlem2  29053  axcontlem4  29055  cncvcOLD  30674  dvcosax  46369