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

Theorem mulassd 7757
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 7719 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1201 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  wcel 1465  (class class class)co 5742  cc 7586   · cmul 7593
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 7691
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  ltmul1  8322  recexap  8382  mulap0  8383  mulcanapd  8390  receuap  8398  divmulasscomap  8424  divdivdivap  8441  divmuleqap  8445  conjmulap  8457  apmul1  8516  qapne  9399  modqmul1  10118  modqdi  10133  expadd  10303  mulbinom2  10376  binom3  10377  faclbnd  10455  faclbnd6  10458  bcm1k  10474  bcp1nk  10476  bcval5  10477  crre  10597  remullem  10611  resqrexlemcalc1  10754  resqrexlemnm  10758  amgm2  10858  binomlem  11220  geo2sum  11251  mertenslemi1  11272  sinadd  11370  tanaddap  11373  dvdsmulcr  11450  dvdsmulgcd  11640  qredeq  11704  2sqpwodd  11781  dvexp  12771  tangtx  12846
  Copyright terms: Public domain W3C validator