Theorem mulridd 8096

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930  1c1 7933   · cmul 7937

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8024  ax-1cn 8025  ax-icn 8027  ax-addcl 8028  ax-mulcl 8030  ax-mulcom 8033  ax-mulass 8035  ax-distr 8036  ax-1rid 8039  ax-cnre 8043

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3171  df-in 3173  df-ss 3180  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-br 4048  df-iota 5237  df-fv 5284  df-ov 5954

This theorem is referenced by:  muladd11  8212  muls1d  8497  ltmul1  8672  mulap0  8734  divrecap  8768  diveqap1  8785  conjmulap  8809  apmul1  8868  qapne  9767  divelunit  10131  modqid  10501  q2submod  10537  addmodlteq  10550  expadd  10733  leexp2r  10745  nnlesq  10795  sqoddm1div8  10845  nn0opthlem1d  10872  faclbnd  10893  faclbnd2  10894  faclbnd6  10896  facavg  10898  bcn0  10907  bcn1  10910  reccn2ap  11668  hash2iun1dif1  11835  binom11  11841  trireciplem  11855  geosergap  11861  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  fprodsplitdc  11951  efzval  12038  tanaddaplem  12093  tanaddap  12094  cos01gt0  12118  absef  12125  1dvds  12160  bitsfzo  12310  bitsmod  12311  bezoutlema  12364  bezoutlemb  12365  gcdmultiple  12385  sqgcd  12394  lcm1  12447  coprmdvds  12458  qredeu  12463  phiprmpw  12588  coprimeprodsq  12624  pc2dvds  12697  sumhashdc  12714  fldivp1  12715  pcfaclem  12716  prmpwdvds  12722  zsssubrg  14391  mulgrhm2  14416  znrrg  14466  dveflem  15242  plyconst  15261  plycolemc  15274  efper  15323  tangtx  15354  logdivlti  15397  rpcxpmul2  15429  relogbexpap  15474  rplogbcxp  15479  0sgm  15501  lgsdir2  15554  lgsquad2lem1  15602  lgsquad3  15605  2sqlem6  15641  2sqlem8  15644  trilpolemclim  16049  trilpolemisumle  16051  trilpolemeq1  16053  trilpolemlt1  16054  redcwlpolemeq1  16067  nconstwlpolemgt0  16077