Theorem mullid 11208

Description: Identity law for multiplication. See mulrid 11207 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 11159	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11187	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 702	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11207	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2798	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099  1c1 11102   · cmul 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-mulcl 11163  ax-mulcom 11165  ax-mulass 11167  ax-distr 11168  ax-1rid 11171  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415

This theorem is referenced by:  mullidi  11215  mullidd  11228  muladd11  11381  1p1times  11382  mul02lem1  11387  cnegex2  11393  mulm1  11656  div1  11905  subdivcomb2  11912  recdiv  11922  divdiv2  11928  conjmul  11933  ser1const  14096  expp1  14106  recan  15390  arisum  15916  geo2sum  15929  prodrblem  15985  prodmolem2a  15990  risefac1  16088  fallfac1  16089  bpoly3  16113  bpoly4  16114  sinhval  16211  coshval  16212  demoivreALT  16258  gcdadd  16585  gcdid  16586  cncrng  21524  cnfld1  21528  blcvx  24936  icccvx  25090  cnlmod  25280  coeidp  26401  dgrid  26402  quartlem1  27000  asinsinlem  27034  asinsin  27035  atantan  27066  musumsum  27334  brbtwn2  29233  axsegconlem1  29245  ax5seglem1  29256  ax5seglem2  29257  ax5seglem4  29260  ax5seglem5  29261  axeuclid  29291  axcontlem2  29293  axcontlem4  29295  cncvcOLD  30913  dvcosax  46620  sin3t  47585  cos3t  47586  sin5tlem4  47590