Theorem mullid 11234

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127  1c1 11130   · cmul 11134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-mulcl 11191  ax-mulcom 11193  ax-mulass 11195  ax-distr 11196  ax-1rid 11199  ax-cnre 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408

This theorem is referenced by:  mullidi  11240  mullidd  11253  muladd11  11405  1p1times  11406  mul02lem1  11411  cnegex2  11417  mulm1  11678  div1  11931  subdivcomb2  11937  recdiv  11947  divdiv2  11953  conjmul  11958  ser1const  14076  expp1  14086  recan  15355  arisum  15876  geo2sum  15889  prodrblem  15945  prodmolem2a  15950  risefac1  16049  fallfac1  16050  bpoly3  16074  bpoly4  16075  sinhval  16172  coshval  16173  demoivreALT  16219  gcdadd  16545  gcdid  16546  cncrng  21351  cncrngOLD  21352  cnfld1  21356  cnfld1OLD  21357  blcvx  24737  icccvx  24899  cnlmod  25091  coeidp  26221  dgrid  26222  quartlem1  26819  asinsinlem  26853  asinsin  26854  atantan  26885  musumsum  27154  brbtwn2  28884  axsegconlem1  28896  ax5seglem1  28907  ax5seglem2  28908  ax5seglem4  28911  ax5seglem5  28912  axeuclid  28942  axcontlem2  28944  axcontlem4  28946  cncvcOLD  30564  dvcosax  45955