Theorem mulridd 8171

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005  1c1 8008   · cmul 8012

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 8099  ax-1cn 8100  ax-icn 8102  ax-addcl 8103  ax-mulcl 8105  ax-mulcom 8108  ax-mulass 8110  ax-distr 8111  ax-1rid 8114  ax-cnre 8118

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  muladd11  8287  muls1d  8572  ltmul1  8747  mulap0  8809  divrecap  8843  diveqap1  8860  conjmulap  8884  apmul1  8943  qapne  9842  divelunit  10206  modqid  10579  q2submod  10615  addmodlteq  10628  expadd  10811  leexp2r  10823  nnlesq  10873  sqoddm1div8  10923  nn0opthlem1d  10950  faclbnd  10971  faclbnd2  10972  faclbnd6  10974  facavg  10976  bcn0  10985  bcn1  10988  reccn2ap  11832  hash2iun1dif1  11999  binom11  12005  trireciplem  12019  geosergap  12025  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  fprodsplitdc  12115  efzval  12202  tanaddaplem  12257  tanaddap  12258  cos01gt0  12282  absef  12289  1dvds  12324  bitsfzo  12474  bitsmod  12475  bezoutlema  12528  bezoutlemb  12529  gcdmultiple  12549  sqgcd  12558  lcm1  12611  coprmdvds  12622  qredeu  12627  phiprmpw  12752  coprimeprodsq  12788  pc2dvds  12861  sumhashdc  12878  fldivp1  12879  pcfaclem  12880  prmpwdvds  12886  zsssubrg  14557  mulgrhm2  14582  znrrg  14632  dveflem  15408  plyconst  15427  plycolemc  15440  efper  15489  tangtx  15520  logdivlti  15563  rpcxpmul2  15595  relogbexpap  15640  rplogbcxp  15645  0sgm  15667  lgsdir2  15720  lgsquad2lem1  15768  lgsquad3  15771  2sqlem6  15807  2sqlem8  15810  trilpolemclim  16434  trilpolemisumle  16436  trilpolemeq1  16438  trilpolemlt1  16439  redcwlpolemeq1  16452  nconstwlpolemgt0  16462