Theorem mullid 11238

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

Assertion

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

Proof of Theorem mullid

Step	Hyp	Ref	Expression
1		ax-1cn 11191	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11219	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 689	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11237	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2768	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  (class class class)co 7415  ℂcc 11131  1c1 11134   · cmul 11138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-mulcl 11195  ax-mulcom 11197  ax-mulass 11199  ax-distr 11200  ax-1rid 11203  ax-cnre 11206

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5144  df-iota 6495  df-fv 6551  df-ov 7418

This theorem is referenced by:  mullidi  11244  mullidd  11257  muladd11  11409  1p1times  11410  mul02lem1  11415  cnegex2  11421  mulm1  11680  div1  11928  subdivcomb2  11935  recdiv  11945  divdiv2  11951  conjmul  11956  ser1const  14050  expp1  14060  recan  15310  arisum  15833  geo2sum  15846  prodrblem  15900  prodmolem2a  15905  risefac1  16004  fallfac1  16005  bpoly3  16029  bpoly4  16030  sinhval  16125  coshval  16126  demoivreALT  16172  gcdadd  16495  gcdid  16496  cncrng  21310  cncrngOLD  21311  cnfld1  21315  cnfld1OLD  21316  blcvx  24708  icccvx  24869  cnlmod  25061  coeidp  26192  dgrid  26193  quartlem1  26783  asinsinlem  26817  asinsin  26818  atantan  26849  musumsum  27118  brbtwn2  28710  axsegconlem1  28722  ax5seglem1  28733  ax5seglem2  28734  ax5seglem4  28737  ax5seglem5  28738  axeuclid  28768  axcontlem2  28770  axcontlem4  28772  cncvcOLD  30387  dvcosax  45305