Theorem mulass 11222

Description: Alias for ax-mulass 11200, for naming consistency with mulassi 11251. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Proof of Theorem mulass

Step	Hyp	Ref	Expression
1		ax-mulass 11200	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132   · cmul 11139

This theorem was proved from axioms:  ax-mulass 11200

This theorem is referenced by:  mulrid  11238  mulassi  11251  mulassd  11263  mul12  11405  mul32  11406  mul31  11407  mul4  11408  00id  11415  divass  11919  cju  12241  div4p1lem1div2  12501  xmulasslem3  13307  mulbinom2  14246  sqoddm1div8  14266  faclbnd5  14321  bcval5  14341  remim  15141  imval2  15175  01sqrexlem7  15272  sqrtneglem  15290  sqreulem  15383  clim2div  15910  prodfmul  15911  prodmolem3  15954  sinhval  16177  coshval  16178  absefib  16221  efieq1re  16222  muldvds1  16305  muldvds2  16306  dvdsmulc  16308  dvdsmulcr  16310  dvdstr  16318  eulerthlem2  16806  oddprmdvds  16928  ablfacrp  20054  cncrng  21356  cncrngOLD  21357  nmoleub2lem3  25071  cnlmod  25096  itg2mulc  25705  abssinper  26487  sinasin  26856  dchrabl  27222  bposlem6  27257  bposlem9  27260  2sqlem6  27391  rpvmasum2  27480  cncvcOLD  30569  ipasslem5  30821  ipasslem11  30826  dvasin  37733  facp2  42161  pellexlem2  42828  jm2.25  42998  expgrowth  44334  2zrngmsgrp  48208  nn0sumshdiglemA  48579