Theorem mulridd 8189

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mulridd	⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Proof of Theorem mulridd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulrid 8169	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023  1c1 8026   · cmul 8030

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8117  ax-1cn 8118  ax-icn 8120  ax-addcl 8121  ax-mulcl 8123  ax-mulcom 8126  ax-mulass 8128  ax-distr 8129  ax-1rid 8132  ax-cnre 8136

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  muladd11  8305  muls1d  8590  ltmul1  8765  mulap0  8827  divrecap  8861  diveqap1  8878  conjmulap  8902  apmul1  8961  qapne  9866  divelunit  10230  modqid  10604  q2submod  10640  addmodlteq  10653  expadd  10836  leexp2r  10848  nnlesq  10898  sqoddm1div8  10948  nn0opthlem1d  10975  faclbnd  10996  faclbnd2  10997  faclbnd6  10999  facavg  11001  bcn0  11010  bcn1  11013  reccn2ap  11867  hash2iun1dif1  12034  binom11  12040  trireciplem  12054  geosergap  12060  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  fprodsplitdc  12150  efzval  12237  tanaddaplem  12292  tanaddap  12293  cos01gt0  12317  absef  12324  1dvds  12359  bitsfzo  12509  bitsmod  12510  bezoutlema  12563  bezoutlemb  12564  gcdmultiple  12584  sqgcd  12593  lcm1  12646  coprmdvds  12657  qredeu  12662  phiprmpw  12787  coprimeprodsq  12823  pc2dvds  12896  sumhashdc  12913  fldivp1  12914  pcfaclem  12915  prmpwdvds  12921  zsssubrg  14592  mulgrhm2  14617  znrrg  14667  dveflem  15443  plyconst  15462  plycolemc  15475  efper  15524  tangtx  15555  logdivlti  15598  rpcxpmul2  15630  relogbexpap  15675  rplogbcxp  15680  0sgm  15702  lgsdir2  15755  lgsquad2lem1  15803  lgsquad3  15806  2sqlem6  15842  2sqlem8  15845  trilpolemclim  16590  trilpolemisumle  16592  trilpolemeq1  16594  trilpolemlt1  16595  redcwlpolemeq1  16608  nconstwlpolemgt0  16618