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

Theorem mulass 7040
Description: Alias for ax-mulass 7015, for naming consistency with mulassi 7064. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulass ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Proof of Theorem mulass
StepHypRef Expression
1 ax-mulass 7015 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 894   = wceq 1257  wcel 1407  (class class class)co 5537  cc 6915   · cmul 6922
This theorem was proved from axioms:  ax-mulass 7015
This theorem is referenced by:  mulid1  7052  mulassi  7064  mulassd  7078  mul12  7173  mul32  7174  mul31  7175  mul4  7176  rimul  7620  divassap  7713  cju  7959  div4p1lem1div2  8205  mulbinom2  9497  sqoddm1div8  9533  remim  9652  imval2  9686  muldvds1  10095  muldvds2  10096  dvdsmulc  10098  dvdstr  10107
  Copyright terms: Public domain W3C validator