Theorem mulass 11293

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

Assertion

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

Proof of Theorem mulass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  (class class class)co 7422  ℂcc 11203   · cmul 11210

This proof depends on axioms:  ax-mulass 11271

This theorem is used by:  mulrid  11311  mulassi  11325  mulassd  11337  mul12  11480  mul32  11481  mul31  11482  mul4  11483  00id  11490  divass  11997  cju  12321  div4p1lem1div2  12606  xmulasslem3  13421  mulbinom2  14372  sqoddm1div8  14392  faclbnd5  14447  bcval5  14467  remim  15291  imval2  15325  01sqrexlem7  15422  sqrtneglem  15440  sqreulem  15534  clim2div  16065  prodfmul  16066  prodmolem3  16107  sinhval  16329  coshval  16330  absefib  16373  efieq1re  16374  muldvds1  16457  muldvds2  16458  dvdsmulc  16460  dvdsmulcr  16462  dvdstr  16471  eulerthlem2  16966  oddprmdvds  17088  ablfacrp  20289  cncrng  21706  nmoleub2lem3  25443  cnlmod  25468  itg2mulc  26075  abssinper  26856  sinasin  27224  dchrabl  27588  bposlem6  27623  bposlem9  27626  2sqlem6  27757  rpvmasum2  27846  cncvcOLD  31192  ipasslem5  31444  ipasslem11  31449  dvasin  38729  facp2  43300  pellexlem2  43944  jm2.25  44113  expgrowth  45426  2zrngmsgrp  49457  nn0sumshdiglemA  49838