Theorem mulid2 10640

Description: Identity law for multiplication. See mulid1 10639 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 10595	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 10623	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 688	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulid1 10639	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2856	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535  1c1 10538   · cmul 10542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-mulcom 10601  ax-mulass 10603  ax-distr 10604  ax-1rid 10607  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  mulid2i  10646  mulid2d  10659  muladd11  10810  1p1times  10811  mul02lem1  10816  cnegex2  10822  mulm1  11081  div1  11329  subdivcomb2  11336  recdiv  11346  divdiv2  11352  conjmul  11357  ser1const  13427  expp1  13437  recan  14696  arisum  15215  geo2sum  15229  prodrblem  15283  prodmolem2a  15288  risefac1  15387  fallfac1  15388  bpoly3  15412  bpoly4  15413  sinhval  15507  coshval  15508  demoivreALT  15554  gcdadd  15874  gcdid  15875  cncrng  20566  cnfld1  20570  blcvx  23406  icccvx  23554  cnlmod  23744  coeidp  24853  dgrid  24854  quartlem1  25435  asinsinlem  25469  asinsin  25470  atantan  25501  musumsum  25769  brbtwn2  26691  axsegconlem1  26703  ax5seglem1  26714  ax5seglem2  26715  ax5seglem4  26718  ax5seglem5  26719  axeuclid  26749  axcontlem2  26751  axcontlem4  26753  cncvcOLD  28360  dvcosax  42231