Theorem mulass 11097

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   · cmul 11014

This theorem was proved from axioms:  ax-mulass 11075

This theorem is referenced by:  mulrid  11113  mulassi  11126  mulassd  11138  mul12  11281  mul32  11282  mul31  11283  mul4  11284  00id  11291  divass  11797  cju  12124  div4p1lem1div2  12379  xmulasslem3  13188  mulbinom2  14130  sqoddm1div8  14150  faclbnd5  14205  bcval5  14225  remim  15024  imval2  15058  01sqrexlem7  15155  sqrtneglem  15173  sqreulem  15267  clim2div  15796  prodfmul  15797  prodmolem3  15840  sinhval  16063  coshval  16064  absefib  16107  efieq1re  16108  muldvds1  16191  muldvds2  16192  dvdsmulc  16194  dvdsmulcr  16196  dvdstr  16205  eulerthlem2  16693  oddprmdvds  16815  ablfacrp  19947  cncrng  21295  cncrngOLD  21296  nmoleub2lem3  25013  cnlmod  25038  itg2mulc  25646  abssinper  26428  sinasin  26797  dchrabl  27163  bposlem6  27198  bposlem9  27201  2sqlem6  27332  rpvmasum2  27421  cncvcOLD  30527  ipasslem5  30779  ipasslem11  30784  dvasin  37684  facp2  42116  pellexlem2  42803  jm2.25  42972  expgrowth  44308  2zrngmsgrp  48237  nn0sumshdiglemA  48604