Theorem mullid 11225

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116  1c1 11119   · cmul 11123

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 2148  ax-9 2156  ax-ext 2738  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-mulcl 11180  ax-mulcom 11182  ax-mulass 11184  ax-distr 11185  ax-1rid 11188  ax-cnre 11191

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 2745  df-cleq 2758  df-clel 2841  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  mullidi  11232  mullidd  11245  muladd11  11398  1p1times  11399  mul02lem1  11404  cnegex2  11410  mulm1  11673  div1  11922  subdivcomb2  11929  recdiv  11939  divdiv2  11945  conjmul  11950  ser1const  14114  expp1  14124  recan  15414  arisum  15940  geo2sum  15953  prodrblem  16009  prodmolem2a  16014  risefac1  16112  fallfac1  16113  bpoly3  16137  bpoly4  16138  sinhval  16235  coshval  16236  demoivreALT  16282  gcdadd  16609  gcdid  16610  cncrng  21580  cnfld1  21584  blcvx  24992  icccvx  25146  cnlmod  25336  coeidp  26457  dgrid  26458  quartlem1  27059  asinsinlem  27093  asinsin  27094  atantan  27125  musumsum  27393  brbtwn2  29292  axsegconlem1  29304  ax5seglem1  29315  ax5seglem2  29316  ax5seglem4  29319  ax5seglem5  29320  axeuclid  29350  axcontlem2  29352  axcontlem4  29354  cncvcOLD  30972  dvcosax  46681  sin3t  47649  cos3t  47650  sin5tlem4  47654