Theorem mullid 11334

Description: Identity law for multiplication. See mulrid 11333 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 11285	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11313	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 703	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11333	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2798	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  1c1 11228   · cmul 11232

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-mulcl 11289  ax-mulcom 11291  ax-mulass 11293  ax-distr 11294  ax-1rid 11297  ax-cnre 11300

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446

This theorem is used by:  mullidi  11341  mullidd  11354  muladd11  11507  1p1times  11508  mul02lem1  11513  cnegex2  11519  mulm1  11784  div1  12033  subdivcomb2  12040  recdiv  12050  divdiv2  12056  conjmul  12061  ser1const  14228  expp1  14238  recan  15533  arisum  16058  geo2sum  16071  prodrblem  16125  prodmolem2a  16130  risefac1  16228  fallfac1  16229  bpoly3  16253  bpoly4  16254  sinhval  16351  coshval  16352  demoivreALT  16398  gcdadd  16727  gcdid  16728  cncrng  21729  cnfld1  21733  blcvx  25147  icccvx  25301  cnlmod  25491  coeidp  26612  dgrid  26613  quartlem1  27215  asinsinlem  27249  asinsin  27250  atantan  27281  musumsum  27549  brbtwn2  29513  axsegconlem1  29525  ax5seglem1  29536  ax5seglem2  29537  ax5seglem4  29540  ax5seglem5  29541  axeuclid  29571  axcontlem2  29573  axcontlem4  29575  cncvcOLD  31215  dvcosax  47141  sin3t  48122  cos3t  48123  sin5tlem4  48127  sqrtnpoly  48148