Theorem mullid 11173

Description: Identity law for multiplication. See mulrid 11172 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 11126	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11154	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 690	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11172	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2764	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   · cmul 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  mullidi  11179  mullidd  11192  muladd11  11344  1p1times  11345  mul02lem1  11350  cnegex2  11356  mulm1  11619  div1  11872  subdivcomb2  11878  recdiv  11888  divdiv2  11894  conjmul  11899  ser1const  14023  expp1  14033  recan  15303  arisum  15826  geo2sum  15839  prodrblem  15895  prodmolem2a  15900  risefac1  15999  fallfac1  16000  bpoly3  16024  bpoly4  16025  sinhval  16122  coshval  16123  demoivreALT  16169  gcdadd  16496  gcdid  16497  cncrng  21300  cncrngOLD  21301  cnfld1  21305  cnfld1OLD  21306  blcvx  24686  icccvx  24848  cnlmod  25040  coeidp  26169  dgrid  26170  quartlem1  26767  asinsinlem  26801  asinsin  26802  atantan  26833  musumsum  27102  brbtwn2  28832  axsegconlem1  28844  ax5seglem1  28855  ax5seglem2  28856  ax5seglem4  28859  ax5seglem5  28860  axeuclid  28890  axcontlem2  28892  axcontlem4  28894  cncvcOLD  30512  dvcosax  45924