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