Theorem mulridi 11316

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mulridi	⊢ (𝐴 · 1) = 𝐴

Proof of Theorem mulridi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mulrid 11309	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 · 1) = 𝐴

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201  1c1 11204   · cmul 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-mulcl 11265  ax-mulcom 11267  ax-mulass 11269  ax-distr 11270  ax-1rid 11273  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  addrid  11493  0lt1  11841  muleqadd  11963  1t1e1  12507  2t1e2  12508  3t1e3  12510  9p1e10  12819  numltc  12848  numsucc  12862  dec10p  12865  numadd  12869  numaddc  12870  11multnc  12890  4t3lem  12919  5t2e10  12922  9t11e99OLD  12953  nn0opthlem1  14415  faclbnd4lem1  14440  sgnmul  15265  rei  15328  imi  15329  cji  15331  sqrtm1  15447  0.999...  16055  efival  16325  ef01bndlem  16357  5ndvds6  16589  3lcm2e6  16913  decsplit0b  17262  2exp8  17271  37prm  17304  43prm  17305  83prm  17306  139prm  17307  163prm  17308  317prm  17309  1259lem1  17314  1259lem2  17315  1259lem3  17316  1259lem4  17317  1259lem5  17318  2503lem1  17320  2503lem2  17321  2503prm  17323  4001lem1  17324  4001lem2  17325  4001lem3  17326  cnmsgnsubg  21888  mdetralt  22928  dveflem  26304  dvsincos  26306  efhalfpi  26805  pige3ALT  26853  cosne0  26862  efif1olem4  26878  logf1o2  26983  asin1  27227  dvatan  27268  log2ublem3  27281  log2ub  27282  birthday  27287  basellem9  27421  ppiub  27536  chtub  27544  bposlem8  27623  lgsdir2  27662  mulog2sumlem2  27867  pntlemb  27929  avril1  31069  ipidsq  31317  nmopadjlem  32696  nmopcoadji  32708  unierri  32711  signswch  35236  itgexpif  35281  reprlt  35294  breprexp  35308  hgt750lem  35326  hgt750lem2  35327  circum  36525  dvasin  38715  3lexlogpow5ineq1  43197  3lexlogpow5ineq5  43203  aks4d1p1  43219  235t711  43455  ex-decpmul  43456  it1ei  43466  sqrtcval2  44735  resqrtvalex  44738  imsqrtvalex  44739  inductionexd  45248  xralrple3  46478  wallispi  47173  wallispi2lem2  47175  stirlinglem1  47177  dirkertrigeqlem3  47203  goldpolyfactor  48020  goldratval  48029  modm1p1ne  48539  257prm  48739  fmtno4prmfac193  48751  fmtno5fac  48760  139prmALT  48774  127prm  48777  2exp340mod341  48924