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

Theorem mulassi 10261
Description: Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1 𝐴 ∈ ℂ
axi.2 𝐵 ∈ ℂ
axi.3 𝐶 ∈ ℂ
Assertion
Ref Expression
mulassi ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

Proof of Theorem mulassi
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 axi.2 . 2 𝐵 ∈ ℂ
3 axi.3 . 2 𝐶 ∈ ℂ
4 mulass 10236 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4mp3an 1573 1 ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wcel 2139  (class class class)co 6814  cc 10146   · cmul 10153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 10214
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074
This theorem is referenced by:  8th4div3  11464  numma  11769  decbin0  11894  sq4e2t8  13176  3dec  13264  3decOLD  13267  faclbnd4lem1  13294  ef01bndlem  15133  3dvdsdec  15276  3dvdsdecOLD  15277  3dvds2dec  15278  3dvds2decOLD  15279  dec5dvds  15990  karatsuba  16014  karatsubaOLD  16015  sincos4thpi  24485  sincos6thpi  24487  ang180lem2  24760  ang180lem3  24761  asin1  24841  efiatan2  24864  2efiatan  24865  log2cnv  24891  log2ublem2  24894  log2ublem3  24895  log2ub  24896  bclbnd  25225  bposlem8  25236  2lgsoddprmlem3d  25358  ax5seglem7  26035  ipasslem10  28024  siilem1  28036  normlem0  28296  normlem9  28305  bcseqi  28307  polid2i  28344  dfdec100  29906  dpmul100  29935  dpmul1000  29937  dpexpp1  29946  dpmul4  29952  quad3  31892  iexpire  31949  fourierswlem  40968  fouriersw  40969  41prothprm  42064  tgoldbachlt  42232  tgoldbachltOLD  42238
  Copyright terms: Public domain W3C validator