Theorem mullid 11260

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   · cmul 11160

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  mullidi  11266  mullidd  11279  muladd11  11431  1p1times  11432  mul02lem1  11437  cnegex2  11443  mulm1  11704  div1  11957  subdivcomb2  11963  recdiv  11973  divdiv2  11979  conjmul  11984  ser1const  14099  expp1  14109  recan  15375  arisum  15896  geo2sum  15909  prodrblem  15965  prodmolem2a  15970  risefac1  16069  fallfac1  16070  bpoly3  16094  bpoly4  16095  sinhval  16190  coshval  16191  demoivreALT  16237  gcdadd  16563  gcdid  16564  cncrng  21401  cncrngOLD  21402  cnfld1  21406  cnfld1OLD  21407  blcvx  24819  icccvx  24981  cnlmod  25173  coeidp  26303  dgrid  26304  quartlem1  26900  asinsinlem  26934  asinsin  26935  atantan  26966  musumsum  27235  brbtwn2  28920  axsegconlem1  28932  ax5seglem1  28943  ax5seglem2  28944  ax5seglem4  28947  ax5seglem5  28948  axeuclid  28978  axcontlem2  28980  axcontlem4  28982  cncvcOLD  30602  dvcosax  45941