Theorem mullid 11143

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   · cmul 11043

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 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  mullidi  11149  mullidd  11162  muladd11  11315  1p1times  11316  mul02lem1  11321  cnegex2  11327  mulm1  11590  div1  11843  subdivcomb2  11849  recdiv  11859  divdiv2  11865  conjmul  11870  ser1const  13993  expp1  14003  recan  15272  arisum  15795  geo2sum  15808  prodrblem  15864  prodmolem2a  15869  risefac1  15968  fallfac1  15969  bpoly3  15993  bpoly4  15994  sinhval  16091  coshval  16092  demoivreALT  16138  gcdadd  16465  gcdid  16466  cncrng  21355  cncrngOLD  21356  cnfld1  21360  cnfld1OLD  21361  blcvx  24754  icccvx  24916  cnlmod  25108  coeidp  26237  dgrid  26238  quartlem1  26835  asinsinlem  26869  asinsin  26870  atantan  26901  musumsum  27170  brbtwn2  28990  axsegconlem1  29002  ax5seglem1  29013  ax5seglem2  29014  ax5seglem4  29017  ax5seglem5  29018  axeuclid  29048  axcontlem2  29050  axcontlem4  29052  cncvcOLD  30670  dvcosax  46278