Theorem mullid 11310

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201  1c1 11204   · cmul 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-mulcl 11265  ax-mulcom 11267  ax-mulass 11269  ax-distr 11270  ax-1rid 11273  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  mullidi  11317  mullidd  11330  muladd11  11483  1p1times  11484  mul02lem1  11489  cnegex2  11495  mulm1  11760  div1  12009  subdivcomb2  12016  recdiv  12026  divdiv2  12032  conjmul  12037  ser1const  14204  expp1  14214  recan  15509  arisum  16034  geo2sum  16047  prodrblem  16101  prodmolem2a  16106  risefac1  16204  fallfac1  16205  bpoly3  16229  bpoly4  16230  sinhval  16327  coshval  16328  demoivreALT  16374  gcdadd  16703  gcdid  16704  cncrng  21704  cnfld1  21708  blcvx  25122  icccvx  25276  cnlmod  25466  coeidp  26587  dgrid  26588  quartlem1  27190  asinsinlem  27224  asinsin  27225  atantan  27256  musumsum  27524  brbtwn2  29488  axsegconlem1  29500  ax5seglem1  29511  ax5seglem2  29512  ax5seglem4  29515  ax5seglem5  29516  axeuclid  29546  axcontlem2  29548  axcontlem4  29550  cncvcOLD  31190  dvcosax  47029  sin3t  48010  cos3t  48011  sin5tlem4  48015  sqrtnpoly  48036