Theorem mulass 11156

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   · cmul 11073

This theorem was proved from axioms:  ax-mulass 11134

This theorem is referenced by:  mulrid  11172  mulassi  11185  mulassd  11197  mul12  11339  mul32  11340  mul31  11341  mul4  11342  00id  11349  divass  11855  cju  12182  div4p1lem1div2  12437  xmulasslem3  13246  mulbinom2  14188  sqoddm1div8  14208  faclbnd5  14263  bcval5  14283  remim  15083  imval2  15117  01sqrexlem7  15214  sqrtneglem  15232  sqreulem  15326  clim2div  15855  prodfmul  15856  prodmolem3  15899  sinhval  16122  coshval  16123  absefib  16166  efieq1re  16167  muldvds1  16250  muldvds2  16251  dvdsmulc  16253  dvdsmulcr  16255  dvdstr  16264  eulerthlem2  16752  oddprmdvds  16874  ablfacrp  19998  cncrng  21300  cncrngOLD  21301  nmoleub2lem3  25015  cnlmod  25040  itg2mulc  25648  abssinper  26430  sinasin  26799  dchrabl  27165  bposlem6  27200  bposlem9  27203  2sqlem6  27334  rpvmasum2  27423  cncvcOLD  30512  ipasslem5  30764  ipasslem11  30769  dvasin  37698  facp2  42131  pellexlem2  42818  jm2.25  42988  expgrowth  44324  2zrngmsgrp  48241  nn0sumshdiglemA  48608