Theorem mullid 11288

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179  1c1 11182   · cmul 11186

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-mulcl 11243  ax-mulcom 11245  ax-mulass 11247  ax-distr 11248  ax-1rid 11251  ax-cnre 11254

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415

This theorem is used by:  mullidi  11295  mullidd  11308  muladd11  11461  1p1times  11462  mul02lem1  11467  cnegex2  11473  mulm1  11738  div1  11987  subdivcomb2  11994  recdiv  12004  divdiv2  12010  conjmul  12015  ser1const  14181  expp1  14191  recan  15484  arisum  16009  geo2sum  16022  prodrblem  16076  prodmolem2a  16081  risefac1  16179  fallfac1  16180  bpoly3  16204  bpoly4  16205  sinhval  16302  coshval  16303  demoivreALT  16349  gcdadd  16678  gcdid  16679  cncrng  21679  cnfld1  21683  blcvx  25097  icccvx  25251  cnlmod  25441  coeidp  26562  dgrid  26563  quartlem1  27167  asinsinlem  27201  asinsin  27202  atantan  27233  musumsum  27501  brbtwn2  29465  axsegconlem1  29477  ax5seglem1  29488  ax5seglem2  29489  ax5seglem4  29492  ax5seglem5  29493  axeuclid  29523  axcontlem2  29525  axcontlem4  29527  cncvcOLD  31167  dvcosax  46880  sin3t  47861  cos3t  47862  sin5tlem4  47866  sqrtnpoly  47887