Theorem mulid2 10974

Description: Identity law for multiplication. See mulid1 10973 for commuted version. (Contributed by NM, 8-Oct-1999.)

Assertion

Ref	Expression
mulid2	⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Proof of Theorem mulid2

Step	Hyp	Ref	Expression
1		ax-1cn 10929	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 10957	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 687	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulid1 10973	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2778	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869  1c1 10872   · cmul 10876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-mulcl 10933  ax-mulcom 10935  ax-mulass 10937  ax-distr 10938  ax-1rid 10941  ax-cnre 10944

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278

This theorem is referenced by:  mulid2i  10980  mulid2d  10993  muladd11  11145  1p1times  11146  mul02lem1  11151  cnegex2  11157  mulm1  11416  div1  11664  subdivcomb2  11671  recdiv  11681  divdiv2  11687  conjmul  11692  ser1const  13779  expp1  13789  recan  15048  arisum  15572  geo2sum  15585  prodrblem  15639  prodmolem2a  15644  risefac1  15743  fallfac1  15744  bpoly3  15768  bpoly4  15769  sinhval  15863  coshval  15864  demoivreALT  15910  gcdadd  16233  gcdid  16234  cncrng  20619  cnfld1  20623  blcvx  23961  icccvx  24113  cnlmod  24303  coeidp  25424  dgrid  25425  quartlem1  26007  asinsinlem  26041  asinsin  26042  atantan  26073  musumsum  26341  brbtwn2  27273  axsegconlem1  27285  ax5seglem1  27296  ax5seglem2  27297  ax5seglem4  27300  ax5seglem5  27301  axeuclid  27331  axcontlem2  27333  axcontlem4  27335  cncvcOLD  28945  dvcosax  43467