Theorem mulridd 8307

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141  1c1 8144   · cmul 8148

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-mulcom 8244  ax-mulass 8246  ax-distr 8247  ax-1rid 8250  ax-cnre 8254

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  muladd11  8423  muls1d  8709  ltmul1  8884  mulap0  8946  divrecap  8982  diveqap1  8999  conjmulap  9023  apmul1  9082  qapne  9992  divelunit  10357  modqid  10738  q2submod  10774  addmodlteq  10787  expadd  10970  leexp2r  10982  nnlesq  11032  sqoddm1div8  11083  nn0opthlem1d  11110  faclbnd  11131  faclbnd2  11132  faclbnd6  11134  facavg  11136  bcn0  11145  bcn1  11148  reccn2ap  12026  hash2iun1dif1  12194  binom11  12200  trireciplem  12214  geosergap  12220  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  fprodsplitdc  12310  efzval  12397  tanaddaplem  12452  tanaddap  12453  cos01gt0  12477  absef  12484  1dvds  12519  bitsfzo  12669  bitsmod  12670  bezoutlema  12723  bezoutlemb  12724  gcdmultiple  12744  sqgcd  12753  lcm1  12806  coprmdvds  12817  qredeu  12822  phiprmpw  12947  coprimeprodsq  12983  pc2dvds  13056  sumhashdc  13073  fldivp1  13074  pcfaclem  13075  prmpwdvds  13081  zsssubrg  14862  mulgrhm2  14887  znrrg  14937  dveflem  15720  plyconst  15739  plycolemc  15752  efper  15801  tangtx  15832  logdivlti  15875  rpcxpmul2  15907  relogbexpap  15952  rplogbcxp  15957  0sgm  15982  lgsdir2  16035  lgsquad2lem1  16083  lgsquad3  16086  2sqlem6  16122  2sqlem8  16125  trilpolemclim  16959  trilpolemisumle  16961  trilpolemeq1  16963  trilpolemlt1  16964  redcwlpolemeq1  16978  nconstwlpolemgt0  16989