Theorem mulass 11117

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   · cmul 11034

This theorem was proved from axioms:  ax-mulass 11095

This theorem is referenced by:  mulrid  11133  mulassi  11147  mulassd  11159  mul12  11302  mul32  11303  mul31  11304  mul4  11305  00id  11312  divass  11818  cju  12146  div4p1lem1div2  12423  xmulasslem3  13229  mulbinom2  14176  sqoddm1div8  14196  faclbnd5  14251  bcval5  14271  remim  15070  imval2  15104  01sqrexlem7  15201  sqrtneglem  15219  sqreulem  15313  clim2div  15845  prodfmul  15846  prodmolem3  15889  sinhval  16112  coshval  16113  absefib  16156  efieq1re  16157  muldvds1  16240  muldvds2  16241  dvdsmulc  16243  dvdsmulcr  16245  dvdstr  16254  eulerthlem2  16743  oddprmdvds  16865  ablfacrp  20034  cncrng  21378  cncrngOLD  21379  nmoleub2lem3  25092  cnlmod  25117  itg2mulc  25724  abssinper  26498  sinasin  26866  dchrabl  27231  bposlem6  27266  bposlem9  27269  2sqlem6  27400  rpvmasum2  27489  cncvcOLD  30669  ipasslem5  30921  ipasslem11  30926  dvasin  38039  facp2  42596  pellexlem2  43276  jm2.25  43445  expgrowth  44780  2zrngmsgrp  48741  nn0sumshdiglemA  49107