Theorem mullid 11177

Description: Identity law for multiplication. See mulrid 11176 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 11128	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11156	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 700	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11176	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2796	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068  1c1 11071   · cmul 11075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-mulcl 11132  ax-mulcom 11134  ax-mulass 11136  ax-distr 11137  ax-1rid 11140  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395

This theorem is referenced by:  mullidi  11184  mullidd  11197  muladd11  11350  1p1times  11351  mul02lem1  11356  cnegex2  11362  mulm1  11625  div1  11877  subdivcomb2  11884  recdiv  11894  divdiv2  11900  conjmul  11905  ser1const  14068  expp1  14078  recan  15347  arisum  15873  geo2sum  15886  prodrblem  15942  prodmolem2a  15947  risefac1  16046  fallfac1  16047  bpoly3  16071  bpoly4  16072  sinhval  16169  coshval  16170  demoivreALT  16216  gcdadd  16543  gcdid  16544  cncrng  21425  cnfld1  21429  blcvx  24838  icccvx  24992  cnlmod  25182  coeidp  26303  dgrid  26304  quartlem1  26899  asinsinlem  26933  asinsin  26934  atantan  26965  musumsum  27233  brbtwn2  29052  axsegconlem1  29064  ax5seglem1  29075  ax5seglem2  29076  ax5seglem4  29079  ax5seglem5  29080  axeuclid  29110  axcontlem2  29112  axcontlem4  29114  cncvcOLD  30732  dvcosax  46464  sin3t  47429  cos3t  47430  sin5tlem4  47434