Theorem mullid 11118

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011  1c1 11014   · cmul 11018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-mulcl 11075  ax-mulcom 11077  ax-mulass 11079  ax-distr 11080  ax-1rid 11083  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355

This theorem is referenced by:  mullidi  11124  mullidd  11137  muladd11  11290  1p1times  11291  mul02lem1  11296  cnegex2  11302  mulm1  11565  div1  11818  subdivcomb2  11824  recdiv  11834  divdiv2  11840  conjmul  11845  ser1const  13967  expp1  13977  recan  15246  arisum  15769  geo2sum  15782  prodrblem  15838  prodmolem2a  15843  risefac1  15942  fallfac1  15943  bpoly3  15967  bpoly4  15968  sinhval  16065  coshval  16066  demoivreALT  16112  gcdadd  16439  gcdid  16440  cncrng  21327  cncrngOLD  21328  cnfld1  21332  cnfld1OLD  21333  blcvx  24714  icccvx  24876  cnlmod  25068  coeidp  26197  dgrid  26198  quartlem1  26795  asinsinlem  26829  asinsin  26830  atantan  26861  musumsum  27130  brbtwn2  28885  axsegconlem1  28897  ax5seglem1  28908  ax5seglem2  28909  ax5seglem4  28912  ax5seglem5  28913  axeuclid  28943  axcontlem2  28945  axcontlem4  28947  cncvcOLD  30565  dvcosax  46048