Theorem mulridi 11231

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 11224	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 · 1) = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116  1c1 11119   · cmul 11123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-mulcl 11180  ax-mulcom 11182  ax-mulass 11184  ax-distr 11185  ax-1rid 11188  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  addrid  11408  0lt1  11754  muleqadd  11876  1t1e1  12420  2t1e2  12421  3t1e3  12423  9p1e10  12731  numltc  12760  numsucc  12774  dec10p  12777  numadd  12781  numaddc  12782  11multnc  12802  4t3lem  12831  5t2e10  12834  9t11e99OLD  12865  nn0opthlem1  14324  faclbnd4lem1  14349  sgnmul  15170  rei  15233  imi  15234  cji  15236  sqrtm1  15352  0.999...  15961  efival  16233  ef01bndlem  16265  5ndvds6  16497  3lcm2e6  16816  decsplit0b  17164  2exp8  17173  37prm  17206  43prm  17207  83prm  17208  139prm  17209  163prm  17210  317prm  17211  1259lem1  17216  1259lem2  17217  1259lem3  17218  1259lem4  17219  1259lem5  17220  2503lem1  17222  2503lem2  17223  2503prm  17225  4001lem1  17226  4001lem2  17227  4001lem3  17228  cnmsgnsubg  21764  mdetralt  22802  dveflem  26175  dvsincos  26177  efhalfpi  26673  pige3ALT  26722  cosne0  26731  efif1olem4  26747  logf1o2  26852  asin1  27096  dvatan  27137  log2ublem3  27150  log2ub  27151  birthday  27156  basellem9  27290  ppiub  27405  chtub  27413  bposlem8  27492  lgsdir2  27531  mulog2sumlem2  27736  pntlemb  27798  avril1  30851  ipidsq  31099  nmopadjlem  32478  nmopcoadji  32490  unierri  32493  signswch  34980  itgexpif  35025  reprlt  35038  breprexp  35052  hgt750lem  35070  hgt750lem2  35071  circum  36187  dvasin  38396  3lexlogpow5ineq1  42862  3lexlogpow5ineq5  42868  aks4d1p1  42884  235t711  43107  ex-decpmul  43108  it1ei  43118  sqrtcval2  44409  resqrtvalex  44412  imsqrtvalex  44413  inductionexd  44922  xralrple3  46130  wallispi  46825  wallispi2lem2  46827  stirlinglem1  46829  dirkertrigeqlem3  46855  modm1p1ne  48154  257prm  48354  fmtno4prmfac193  48366  fmtno5fac  48375  139prmALT  48389  127prm  48392  2exp340mod341  48539