ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulassd GIF version

Theorem mulassd 7980
Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
addcld.2 (𝜑𝐵 ∈ ℂ)
addassd.3 (𝜑𝐶 ∈ ℂ)
Assertion
Ref Expression
mulassd (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Proof of Theorem mulassd
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addassd.3 . 2 (𝜑𝐶 ∈ ℂ)
4 mulass 7941 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1238 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353  wcel 2148  (class class class)co 5874  cc 7808   · cmul 7815
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-mulass 7913
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  ltmul1  8548  recexap  8609  mulap0  8610  mulcanapd  8617  receuap  8625  divmulasscomap  8652  divdivdivap  8669  divmuleqap  8673  conjmulap  8685  apmul1  8744  qapne  9638  modqmul1  10376  modqdi  10391  expadd  10561  mulbinom2  10636  binom3  10637  faclbnd  10720  faclbnd6  10723  bcm1k  10739  bcp1nk  10741  bcval5  10742  crre  10865  remullem  10879  resqrexlemcalc1  11022  resqrexlemnm  11026  amgm2  11126  binomlem  11490  geo2sum  11521  mertenslemi1  11542  clim2prod  11546  sinadd  11743  tanaddap  11746  dvdsmulcr  11827  dvdsmulgcd  12025  qredeq  12095  2sqpwodd  12175  pcaddlem  12337  prmpwdvds  12352  dvexp  14111  tangtx  14195  cxpmul  14269  binom4  14333  lgsneg  14361  lgseisenlem1  14386  lgseisenlem2  14387  2lgsoddprmlem2  14390  2sqlem3  14400
  Copyright terms: Public domain W3C validator