Theorem mullid 11257

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  1c1 11153   · cmul 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-mulcom 11216  ax-mulass 11218  ax-distr 11219  ax-1rid 11222  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  mullidi  11263  mullidd  11276  muladd11  11428  1p1times  11429  mul02lem1  11434  cnegex2  11440  mulm1  11701  div1  11954  subdivcomb2  11960  recdiv  11970  divdiv2  11976  conjmul  11981  ser1const  14095  expp1  14105  recan  15371  arisum  15892  geo2sum  15905  prodrblem  15961  prodmolem2a  15966  risefac1  16065  fallfac1  16066  bpoly3  16090  bpoly4  16091  sinhval  16186  coshval  16187  demoivreALT  16233  gcdadd  16559  gcdid  16560  cncrng  21418  cncrngOLD  21419  cnfld1  21423  cnfld1OLD  21424  blcvx  24833  icccvx  24994  cnlmod  25186  coeidp  26317  dgrid  26318  quartlem1  26914  asinsinlem  26948  asinsin  26949  atantan  26980  musumsum  27249  brbtwn2  28934  axsegconlem1  28946  ax5seglem1  28957  ax5seglem2  28958  ax5seglem4  28961  ax5seglem5  28962  axeuclid  28992  axcontlem2  28994  axcontlem4  28996  cncvcOLD  30611  dvcosax  45881