Theorem mulid2 10230

Description: Identity law for multiplication. Note: see mulid1 10229 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 10186	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 10214	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 708	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulid1 10229	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2794	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2139  (class class class)co 6813  ℂcc 10126  1c1 10129   · cmul 10133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-mulcl 10190  ax-mulcom 10192  ax-mulass 10194  ax-distr 10195  ax-1rid 10198  ax-cnre 10201

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816

This theorem is referenced by:  mulid2i  10235  mulid2d  10250  muladd11  10398  1p1times  10399  mul02lem1  10404  cnegex2  10410  mulm1  10663  div1  10908  recdiv  10923  divdiv2  10929  conjmul  10934  ser1const  13051  expp1  13061  recan  14275  arisum  14791  geo2sum  14803  prodrblem  14858  prodmolem2a  14863  risefac1  14963  fallfac1  14964  bpoly3  14988  bpoly4  14989  sinhval  15083  coshval  15084  demoivreALT  15130  gcdadd  15449  gcdid  15450  cncrng  19969  cnfld1  19973  cnfldmulg  19980  blcvx  22802  icccvx  22950  cnlmod  23140  coeidp  24218  dgrid  24219  quartlem1  24783  asinsinlem  24817  asinsin  24818  atantan  24849  musumsum  25117  brbtwn2  25984  axsegconlem1  25996  ax5seglem1  26007  ax5seglem2  26008  ax5seglem4  26011  ax5seglem5  26012  axeuclid  26042  axcontlem2  26044  axcontlem4  26046  cncvcOLD  27747  subdivcomb2  31919  dvcosax  40644