Theorem mulid2 10797

Description: Identity law for multiplication. See mulid1 10796 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 10752	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 10780	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 690	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulid1 10796	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2771	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112  (class class class)co 7191  ℂcc 10692  1c1 10695   · cmul 10699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-mulcl 10756  ax-mulcom 10758  ax-mulass 10760  ax-distr 10761  ax-1rid 10764  ax-cnre 10767

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194

This theorem is referenced by:  mulid2i  10803  mulid2d  10816  muladd11  10967  1p1times  10968  mul02lem1  10973  cnegex2  10979  mulm1  11238  div1  11486  subdivcomb2  11493  recdiv  11503  divdiv2  11509  conjmul  11514  ser1const  13597  expp1  13607  recan  14865  arisum  15387  geo2sum  15400  prodrblem  15454  prodmolem2a  15459  risefac1  15558  fallfac1  15559  bpoly3  15583  bpoly4  15584  sinhval  15678  coshval  15679  demoivreALT  15725  gcdadd  16048  gcdid  16049  cncrng  20338  cnfld1  20342  blcvx  23649  icccvx  23801  cnlmod  23991  coeidp  25111  dgrid  25112  quartlem1  25694  asinsinlem  25728  asinsin  25729  atantan  25760  musumsum  26028  brbtwn2  26950  axsegconlem1  26962  ax5seglem1  26973  ax5seglem2  26974  ax5seglem4  26977  ax5seglem5  26978  axeuclid  27008  axcontlem2  27010  axcontlem4  27012  cncvcOLD  28618  dvcosax  43085