Theorem mulass 11155

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  (class class class)co 7391  ℂcc 11065   · cmul 11072

This theorem was proved from axioms:  ax-mulass 11133

This theorem is referenced by:  mulrid  11173  mulassi  11187  mulassd  11199  mul12  11342  mul32  11343  mul31  11344  mul4  11345  00id  11352  divass  11857  cju  12185  div4p1lem1div2  12470  xmulasslem3  13283  mulbinom2  14230  sqoddm1div8  14250  faclbnd5  14305  bcval5  14325  remim  15135  imval2  15169  01sqrexlem7  15266  sqrtneglem  15284  sqreulem  15378  clim2div  15910  prodfmul  15911  prodmolem3  15954  sinhval  16177  coshval  16178  absefib  16221  efieq1re  16222  muldvds1  16305  muldvds2  16306  dvdsmulc  16308  dvdsmulcr  16310  dvdstr  16319  eulerthlem2  16808  oddprmdvds  16930  ablfacrp  20099  cncrng  21433  nmoleub2lem3  25165  cnlmod  25190  itg2mulc  25797  abssinper  26574  sinasin  26942  dchrabl  27306  bposlem6  27341  bposlem9  27344  2sqlem6  27475  rpvmasum2  27564  cncvcOLD  30743  ipasslem5  30995  ipasslem11  31000  dvasin  38164  facp2  42721  pellexlem2  43368  jm2.25  43537  expgrowth  44872  2zrngmsgrp  48836  nn0sumshdiglemA  49202