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

Theorem mulassd 7796
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 7758 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4syl3anc 1216 1 (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331  wcel 1480  (class class class)co 5774  cc 7625   · cmul 7632
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 7730
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  ltmul1  8361  recexap  8421  mulap0  8422  mulcanapd  8429  receuap  8437  divmulasscomap  8463  divdivdivap  8480  divmuleqap  8484  conjmulap  8496  apmul1  8555  qapne  9438  modqmul1  10157  modqdi  10172  expadd  10342  mulbinom2  10415  binom3  10416  faclbnd  10494  faclbnd6  10497  bcm1k  10513  bcp1nk  10515  bcval5  10516  crre  10636  remullem  10650  resqrexlemcalc1  10793  resqrexlemnm  10797  amgm2  10897  binomlem  11259  geo2sum  11290  mertenslemi1  11311  clim2prod  11315  sinadd  11450  tanaddap  11453  dvdsmulcr  11530  dvdsmulgcd  11720  qredeq  11784  2sqpwodd  11861  dvexp  12854  tangtx  12932
  Copyright terms: Public domain W3C validator