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

Theorem mulassd 7901
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 7863 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1220 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1335  wcel 2128  (class class class)co 5824  cc 7730   · cmul 7737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-mulass 7835
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  ltmul1  8467  recexap  8527  mulap0  8528  mulcanapd  8535  receuap  8543  divmulasscomap  8569  divdivdivap  8586  divmuleqap  8590  conjmulap  8602  apmul1  8661  qapne  9548  modqmul1  10276  modqdi  10291  expadd  10461  mulbinom2  10534  binom3  10535  faclbnd  10615  faclbnd6  10618  bcm1k  10634  bcp1nk  10636  bcval5  10637  crre  10757  remullem  10771  resqrexlemcalc1  10914  resqrexlemnm  10918  amgm2  11018  binomlem  11380  geo2sum  11411  mertenslemi1  11432  clim2prod  11436  sinadd  11633  tanaddap  11636  dvdsmulcr  11717  dvdsmulgcd  11909  qredeq  11973  2sqpwodd  12051  dvexp  13086  tangtx  13170  cxpmul  13244  binom4  13307
  Copyright terms: Public domain W3C validator