Theorem mulass 11126

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

This theorem was proved from axioms:  ax-mulass 11104

This theorem is referenced by:  mulrid  11142  mulassi  11155  mulassd  11167  mul12  11310  mul32  11311  mul31  11312  mul4  11313  00id  11320  divass  11826  cju  12153  div4p1lem1div2  12408  xmulasslem3  13213  mulbinom2  14158  sqoddm1div8  14178  faclbnd5  14233  bcval5  14253  remim  15052  imval2  15086  01sqrexlem7  15183  sqrtneglem  15201  sqreulem  15295  clim2div  15824  prodfmul  15825  prodmolem3  15868  sinhval  16091  coshval  16092  absefib  16135  efieq1re  16136  muldvds1  16219  muldvds2  16220  dvdsmulc  16222  dvdsmulcr  16224  dvdstr  16233  eulerthlem2  16721  oddprmdvds  16843  ablfacrp  20009  cncrng  21355  cncrngOLD  21356  nmoleub2lem3  25083  cnlmod  25108  itg2mulc  25716  abssinper  26498  sinasin  26867  dchrabl  27233  bposlem6  27268  bposlem9  27271  2sqlem6  27402  rpvmasum2  27491  cncvcOLD  30671  ipasslem5  30923  ipasslem11  30928  dvasin  37955  facp2  42513  pellexlem2  43187  jm2.25  43356  expgrowth  44691  2zrngmsgrp  48613  nn0sumshdiglemA  48979