Theorem mullid 11134

Description: Identity law for multiplication. See mulrid 11133 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 11087	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11115	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 691	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11133	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2772	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027  1c1 11030   · cmul 11034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-mulcom 11093  ax-mulass 11095  ax-distr 11096  ax-1rid 11099  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363

This theorem is referenced by:  mullidi  11141  mullidd  11154  muladd11  11307  1p1times  11308  mul02lem1  11313  cnegex2  11319  mulm1  11582  div1  11835  subdivcomb2  11842  recdiv  11852  divdiv2  11858  conjmul  11863  ser1const  14011  expp1  14021  recan  15290  arisum  15816  geo2sum  15829  prodrblem  15885  prodmolem2a  15890  risefac1  15989  fallfac1  15990  bpoly3  16014  bpoly4  16015  sinhval  16112  coshval  16113  demoivreALT  16159  gcdadd  16486  gcdid  16487  cncrng  21378  cncrngOLD  21379  cnfld1  21383  cnfld1OLD  21384  blcvx  24773  icccvx  24927  cnlmod  25117  coeidp  26238  dgrid  26239  quartlem1  26834  asinsinlem  26868  asinsin  26869  atantan  26900  musumsum  27169  brbtwn2  28988  axsegconlem1  29000  ax5seglem1  29011  ax5seglem2  29012  ax5seglem4  29015  ax5seglem5  29016  axeuclid  29046  axcontlem2  29048  axcontlem4  29050  cncvcOLD  30669  dvcosax  46372  sin3t  47335  cos3t  47336  sin5tlem4  47340