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

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

Proof of Theorem mulass
StepHypRef Expression
1 ax-mulass 7351 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920   = wceq 1285  wcel 1434  (class class class)co 5591  cc 7251   · cmul 7258
This theorem was proved from axioms:  ax-mulass 7351
This theorem is referenced by:  mulid1  7388  mulassi  7400  mulassd  7414  mul12  7514  mul32  7515  mul31  7516  mul4  7517  rimul  7962  divassap  8055  cju  8315  div4p1lem1div2  8561  mulbinom2  9905  sqoddm1div8  9941  remim  10121  imval2  10155  muldvds1  10601  muldvds2  10602  dvdsmulc  10604  dvdstr  10613
  Copyright terms: Public domain W3C validator