Theorem mulass 10959

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869   · cmul 10876

This theorem was proved from axioms:  ax-mulass 10937

This theorem is referenced by:  mulid1  10973  mulassi  10986  mulassd  10998  mul12  11140  mul32  11141  mul31  11142  mul4  11143  00id  11150  divass  11651  cju  11969  div4p1lem1div2  12228  xmulasslem3  13020  mulbinom2  13938  sqoddm1div8  13958  faclbnd5  14012  bcval5  14032  remim  14828  imval2  14862  sqrlem7  14960  sqrtneglem  14978  sqreulem  15071  clim2div  15601  prodfmul  15602  prodmolem3  15643  sinhval  15863  coshval  15864  absefib  15907  efieq1re  15908  muldvds1  15990  muldvds2  15991  dvdsmulc  15993  dvdsmulcr  15995  dvdstr  16003  eulerthlem2  16483  oddprmdvds  16604  ablfacrp  19669  cncrng  20619  nmoleub2lem3  24278  cnlmod  24303  itg2mulc  24912  abssinper  25677  sinasin  26039  dchrabl  26402  bposlem6  26437  bposlem9  26440  2sqlem6  26571  rpvmasum2  26660  cncvcOLD  28945  ipasslem5  29197  ipasslem11  29202  dvasin  35861  facp2  40099  fac2xp3  40160  pellexlem2  40652  jm2.25  40821  expgrowth  41953  2zrngmsgrp  45505  nn0sumshdiglemA  45965