Theorem mulridi 8186

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

Syntax hints:   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035  1c1 8038   · cmul 8042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-resscn 8129  ax-1cn 8130  ax-icn 8132  ax-addcl 8133  ax-mulcl 8135  ax-mulcom 8138  ax-mulass 8140  ax-distr 8141  ax-1rid 8144  ax-cnre 8148

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-iota 5288  df-fv 5336  df-ov 6026

This theorem is referenced by:  rimul  8770  muleqadd  8853  1t1e1  9301  2t1e2  9302  3t1e3  9304  halfpm6th  9369  iap0  9372  9p1e10  9618  numltc  9641  numsucc  9655  dec10p  9658  numadd  9662  numaddc  9663  11multnc  9683  4t3lem  9712  5t2e10  9715  9t11e99  9745  rei  11482  imi  11483  cji  11485  0.999...  12105  efival  12316  ef01bndlem  12340  5ndvds6  12519  3lcm2e6  12755  decsplit0b  13022  2exp8  13031  dveflem  15479  efhalfpi  15552