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

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

Proof of Theorem mulass
StepHypRef Expression
1 ax-mulass 7448 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 924   = wceq 1289  wcel 1438  (class class class)co 5652  cc 7348   · cmul 7355
This theorem was proved from axioms:  ax-mulass 7448
This theorem is referenced by:  mulid1  7485  mulassi  7497  mulassd  7511  mul12  7611  mul32  7612  mul31  7613  mul4  7614  rimul  8062  divassap  8157  cju  8421  div4p1lem1div2  8669  mulbinom2  10070  sqoddm1div8  10106  remim  10294  imval2  10328  absefib  11060  efieq1re  11061  muldvds1  11099  muldvds2  11100  dvdsmulc  11102  dvdstr  11111
  Copyright terms: Public domain W3C validator