Theorem mulridd 8201

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 8181	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Syntax hints:   → wi 4   = 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:  muladd11  8317  muls1d  8602  ltmul1  8777  mulap0  8839  divrecap  8873  diveqap1  8890  conjmulap  8914  apmul1  8973  qapne  9878  divelunit  10242  modqid  10617  q2submod  10653  addmodlteq  10666  expadd  10849  leexp2r  10861  nnlesq  10911  sqoddm1div8  10961  nn0opthlem1d  10988  faclbnd  11009  faclbnd2  11010  faclbnd6  11012  facavg  11014  bcn0  11023  bcn1  11026  reccn2ap  11896  hash2iun1dif1  12064  binom11  12070  trireciplem  12084  geosergap  12090  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  fprodsplitdc  12180  efzval  12267  tanaddaplem  12322  tanaddap  12323  cos01gt0  12347  absef  12354  1dvds  12389  bitsfzo  12539  bitsmod  12540  bezoutlema  12593  bezoutlemb  12594  gcdmultiple  12614  sqgcd  12623  lcm1  12676  coprmdvds  12687  qredeu  12692  phiprmpw  12817  coprimeprodsq  12853  pc2dvds  12926  sumhashdc  12943  fldivp1  12944  pcfaclem  12945  prmpwdvds  12951  zsssubrg  14623  mulgrhm2  14648  znrrg  14698  dveflem  15479  plyconst  15498  plycolemc  15511  efper  15560  tangtx  15591  logdivlti  15634  rpcxpmul2  15666  relogbexpap  15711  rplogbcxp  15716  0sgm  15738  lgsdir2  15791  lgsquad2lem1  15839  lgsquad3  15842  2sqlem6  15878  2sqlem8  15881  trilpolemclim  16707  trilpolemisumle  16709  trilpolemeq1  16711  trilpolemlt1  16712  redcwlpolemeq1  16726  nconstwlpolemgt0  16736