Theorem mullid 11235

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126  1c1 11129   · cmul 11133

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 2734  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-mulcl 11190  ax-mulcom 11192  ax-mulass 11194  ax-distr 11195  ax-1rid 11198  ax-cnre 11201

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 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420

This theorem is used by:  mullidi  11242  mullidd  11255  muladd11  11408  1p1times  11409  mul02lem1  11414  cnegex2  11420  mulm1  11683  div1  11932  subdivcomb2  11939  recdiv  11949  divdiv2  11955  conjmul  11960  ser1const  14126  expp1  14136  recan  15428  arisum  15953  geo2sum  15966  prodrblem  16022  prodmolem2a  16027  risefac1  16125  fallfac1  16126  bpoly3  16150  bpoly4  16151  sinhval  16248  coshval  16249  demoivreALT  16295  gcdadd  16622  gcdid  16623  cncrng  21612  cnfld1  21616  blcvx  25030  icccvx  25184  cnlmod  25374  coeidp  26496  dgrid  26497  quartlem1  27102  asinsinlem  27136  asinsin  27137  atantan  27168  musumsum  27436  brbtwn2  29370  axsegconlem1  29382  ax5seglem1  29393  ax5seglem2  29394  ax5seglem4  29397  ax5seglem5  29398  axeuclid  29428  axcontlem2  29430  axcontlem4  29432  cncvcOLD  31072  dvcosax  46762  sin3t  47743  cos3t  47744  sin5tlem4  47748  sqrtnpoly  47769