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

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

Proof of Theorem mulass
StepHypRef Expression
1 ax-mulass 7818 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 963   = wceq 1335   ∈ wcel 2128  (class class class)co 5818  ℂcc 7713   · cmul 7720 This theorem was proved from axioms:  ax-mulass 7818 This theorem is referenced by:  mulid1  7858  mulassi  7870  mulassd  7884  mul12  7987  mul32  7988  mul31  7989  mul4  7990  rimul  8443  divassap  8546  cju  8815  div4p1lem1div2  9069  mulbinom2  10516  sqoddm1div8  10553  remim  10742  imval2  10776  clim2divap  11419  prod3fmul  11420  prodmodclem3  11454  absefib  11649  efieq1re  11650  muldvds1  11693  muldvds2  11694  dvdsmulc  11696  dvdstr  11705  abssinper  13127
 Copyright terms: Public domain W3C validator