Theorem mulass 11203

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

Assertion

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

Proof of Theorem mulass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  (class class class)co 7419  ℂcc 11113   · cmul 11120

This proof depends on axioms:  ax-mulass 11181

This theorem is used by:  mulrid  11221  mulassi  11235  mulassd  11247  mul12  11390  mul32  11391  mul31  11392  mul4  11393  00id  11400  divass  11905  cju  12229  div4p1lem1div2  12514  xmulasslem3  13328  mulbinom2  14277  sqoddm1div8  14297  faclbnd5  14352  bcval5  14372  remim  15192  imval2  15226  01sqrexlem7  15323  sqrtneglem  15341  sqreulem  15435  clim2div  15966  prodfmul  15967  prodmolem3  16010  sinhval  16232  coshval  16233  absefib  16276  efieq1re  16277  muldvds1  16360  muldvds2  16361  dvdsmulc  16363  dvdsmulcr  16365  dvdstr  16374  eulerthlem2  16863  oddprmdvds  16985  ablfacrp  20182  cncrng  21593  nmoleub2lem3  25325  cnlmod  25350  itg2mulc  25957  abssinper  26737  sinasin  27105  dchrabl  27469  bposlem6  27504  bposlem9  27507  2sqlem6  27638  rpvmasum2  27727  cncvcOLD  31006  ipasslem5  31258  ipasslem11  31263  dvasin  38412  facp2  42968  pellexlem2  43615  jm2.25  43784  expgrowth  45103  2zrngmsgrp  49075  nn0sumshdiglemA  49456