MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulass Structured version   Visualization version   GIF version

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

Proof of Theorem mulass
StepHypRef Expression
1 ax-mulass 10592 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1538  wcel 2114  (class class class)co 7140  cc 10524   · cmul 10531
This theorem was proved from axioms:  ax-mulass 10592
This theorem is referenced by:  mulid1  10628  mulassi  10641  mulassd  10653  mul12  10794  mul32  10795  mul31  10796  mul4  10797  00id  10804  divass  11305  cju  11621  div4p1lem1div2  11880  xmulasslem3  12667  mulbinom2  13580  sqoddm1div8  13600  faclbnd5  13654  bcval5  13674  remim  14467  imval2  14501  sqrlem7  14599  sqrtneglem  14617  sqreulem  14710  clim2div  15236  prodfmul  15237  prodmolem3  15278  sinhval  15498  coshval  15499  absefib  15542  efieq1re  15543  muldvds1  15625  muldvds2  15626  dvdsmulc  15628  dvdsmulcr  15630  dvdstr  15637  eulerthlem2  16108  oddprmdvds  16228  ablfacrp  19179  cncrng  20110  nmoleub2lem3  23718  cnlmod  23743  itg2mulc  24349  abssinper  25111  sinasin  25473  dchrabl  25836  bposlem6  25871  bposlem9  25874  2sqlem6  26005  rpvmasum2  26094  cncvcOLD  28364  ipasslem5  28616  ipasslem11  28621  dvasin  35099  facp2  39306  fac2xp3  39335  pellexlem2  39701  jm2.25  39870  expgrowth  40973  2zrngmsgrp  44510  nn0sumshdiglemA  44972
  Copyright terms: Public domain W3C validator