Theorem mullid 11226

Description: Identity law for multiplication. See mulrid 11225 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 11179	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11207	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 690	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11225	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2769	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7399  ℂcc 11119  1c1 11122   · cmul 11126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-resscn 11178  ax-1cn 11179  ax-icn 11180  ax-addcl 11181  ax-mulcl 11183  ax-mulcom 11185  ax-mulass 11187  ax-distr 11188  ax-1rid 11191  ax-cnre 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-iota 6480  df-fv 6535  df-ov 7402

This theorem is referenced by:  mullidi  11232  mullidd  11245  muladd11  11397  1p1times  11398  mul02lem1  11403  cnegex2  11409  mulm1  11670  div1  11923  subdivcomb2  11929  recdiv  11939  divdiv2  11945  conjmul  11950  ser1const  14065  expp1  14075  recan  15342  arisum  15863  geo2sum  15876  prodrblem  15932  prodmolem2a  15937  risefac1  16036  fallfac1  16037  bpoly3  16061  bpoly4  16062  sinhval  16157  coshval  16158  demoivreALT  16204  gcdadd  16530  gcdid  16531  cncrng  21336  cncrngOLD  21337  cnfld1  21341  cnfld1OLD  21342  blcvx  24722  icccvx  24884  cnlmod  25076  coeidp  26206  dgrid  26207  quartlem1  26803  asinsinlem  26837  asinsin  26838  atantan  26869  musumsum  27138  brbtwn2  28816  axsegconlem1  28828  ax5seglem1  28839  ax5seglem2  28840  ax5seglem4  28843  ax5seglem5  28844  axeuclid  28874  axcontlem2  28876  axcontlem4  28878  cncvcOLD  30496  dvcosax  45885