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

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

Proof of Theorem mulass
StepHypRef Expression
1 ax-mulass 7691 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 947   = wceq 1316  wcel 1465  (class class class)co 5742  cc 7586   · cmul 7593
This theorem was proved from axioms:  ax-mulass 7691
This theorem is referenced by:  mulid1  7731  mulassi  7743  mulassd  7757  mul12  7859  mul32  7860  mul31  7861  mul4  7862  rimul  8315  divassap  8418  cju  8687  div4p1lem1div2  8941  mulbinom2  10376  sqoddm1div8  10412  remim  10600  imval2  10634  absefib  11404  efieq1re  11405  muldvds1  11445  muldvds2  11446  dvdsmulc  11448  dvdstr  11457  abssinper  12854
  Copyright terms: Public domain W3C validator