Theorem mulid2 9917

Description: Identity law for multiplication. Note: see mulid1 9916 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 9873	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 9901	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 702	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulid1 9916	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2644	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813  1c1 9816   · cmul 9820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-mulcom 9879  ax-mulass 9881  ax-distr 9882  ax-1rid 9885  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  mulid2i  9922  mulid2d  9937  muladd11  10085  1p1times  10086  mul02lem1  10091  cnegex2  10097  mulm1  10350  div1  10595  recdiv  10610  divdiv2  10616  conjmul  10621  ser1const  12719  expp1  12729  recan  13924  arisum  14431  geo2sum  14443  prodrblem  14498  prodmolem2a  14503  risefac1  14603  fallfac1  14604  bpoly3  14628  bpoly4  14629  sinhval  14723  coshval  14724  demoivreALT  14770  gcdadd  15085  gcdid  15086  cncrng  19586  cnfld1  19590  cnfldmulg  19597  blcvx  22409  icccvx  22557  cnlmod  22748  coeidp  23823  dgrid  23824  quartlem1  24384  asinsinlem  24418  asinsin  24419  atantan  24450  musumsum  24718  brbtwn2  25585  axsegconlem1  25597  ax5seglem1  25608  ax5seglem2  25609  ax5seglem4  25612  ax5seglem5  25613  axeuclid  25643  axcontlem2  25645  axcontlem4  25647  cncvcOLD  26822  subdivcomb2  30865  dvcosax  38816