Theorem mulridd 8036

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870  1c1 7873   · cmul 7877

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7964  ax-1cn 7965  ax-icn 7967  ax-addcl 7968  ax-mulcl 7970  ax-mulcom 7973  ax-mulass 7975  ax-distr 7976  ax-1rid 7979  ax-cnre 7983

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921

This theorem is referenced by:  muladd11  8152  ltmul1  8611  mulap0  8673  divrecap  8707  diveqap1  8724  conjmulap  8748  apmul1  8807  qapne  9704  divelunit  10068  modqid  10420  q2submod  10456  addmodlteq  10469  expadd  10652  leexp2r  10664  nnlesq  10714  sqoddm1div8  10764  nn0opthlem1d  10791  faclbnd  10812  faclbnd2  10813  faclbnd6  10815  facavg  10817  bcn0  10826  bcn1  10829  reccn2ap  11456  hash2iun1dif1  11623  binom11  11629  trireciplem  11643  geosergap  11649  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  fprodsplitdc  11739  efzval  11826  tanaddaplem  11881  tanaddap  11882  cos01gt0  11906  absef  11913  1dvds  11948  bezoutlema  12136  bezoutlemb  12137  gcdmultiple  12157  sqgcd  12166  lcm1  12219  coprmdvds  12230  qredeu  12235  phiprmpw  12360  coprimeprodsq  12395  pc2dvds  12468  sumhashdc  12485  fldivp1  12486  pcfaclem  12487  prmpwdvds  12493  zsssubrg  14073  mulgrhm2  14098  znrrg  14148  dveflem  14872  plyconst  14891  efper  14942  tangtx  14973  logdivlti  15016  relogbexpap  15090  rplogbcxp  15095  lgsdir2  15149  2sqlem6  15207  2sqlem8  15210  trilpolemclim  15526  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  redcwlpolemeq1  15544  nconstwlpolemgt0  15554