Theorem mullid 11211

Description: Identity law for multiplication. See mulrid 11210 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 11165	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11193	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 687	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11210	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2764	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7402  ℂcc 11105  1c1 11108   · cmul 11112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-mulcl 11169  ax-mulcom 11171  ax-mulass 11173  ax-distr 11174  ax-1rid 11177  ax-cnre 11180

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-iota 6486  df-fv 6542  df-ov 7405

This theorem is referenced by:  mullidi  11217  mullidd  11230  muladd11  11382  1p1times  11383  mul02lem1  11388  cnegex2  11394  mulm1  11653  div1  11901  subdivcomb2  11908  recdiv  11918  divdiv2  11924  conjmul  11929  ser1const  14022  expp1  14032  recan  15281  arisum  15804  geo2sum  15817  prodrblem  15871  prodmolem2a  15876  risefac1  15975  fallfac1  15976  bpoly3  16000  bpoly4  16001  sinhval  16096  coshval  16097  demoivreALT  16143  gcdadd  16466  gcdid  16467  cncrng  21252  cnfld1  21256  blcvx  24638  icccvx  24799  cnlmod  24991  coeidp  26120  dgrid  26121  quartlem1  26708  asinsinlem  26742  asinsin  26743  atantan  26774  musumsum  27043  brbtwn2  28635  axsegconlem1  28647  ax5seglem1  28658  ax5seglem2  28659  ax5seglem4  28662  ax5seglem5  28663  axeuclid  28693  axcontlem2  28695  axcontlem4  28697  cncvcOLD  30308  gg-cncrng  35674  gg-cnfld1  35675  dvcosax  45152