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

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

Proof of Theorem mulass
StepHypRef Expression
1 ax-mulass 7687 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 945   = wceq 1314  wcel 1463  (class class class)co 5740  cc 7582   · cmul 7589
This theorem was proved from axioms:  ax-mulass 7687
This theorem is referenced by:  mulid1  7727  mulassi  7739  mulassd  7753  mul12  7855  mul32  7856  mul31  7857  mul4  7858  rimul  8310  divassap  8410  cju  8676  div4p1lem1div2  8924  mulbinom2  10348  sqoddm1div8  10384  remim  10572  imval2  10606  absefib  11375  efieq1re  11376  muldvds1  11414  muldvds2  11415  dvdsmulc  11417  dvdstr  11426
  Copyright terms: Public domain W3C validator