Theorem mulass 11281

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

Assertion

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

Proof of Theorem mulass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  (class class class)co 7418  ℂcc 11191   · cmul 11198

This proof depends on axioms:  ax-mulass 11259

This theorem is used by:  mulrid  11299  mulassi  11313  mulassd  11325  mul12  11468  mul32  11469  mul31  11470  mul4  11471  00id  11478  divass  11985  cju  12309  div4p1lem1div2  12594  xmulasslem3  13409  mulbinom2  14360  sqoddm1div8  14380  faclbnd5  14435  bcval5  14455  remim  15277  imval2  15311  01sqrexlem7  15408  sqrtneglem  15426  sqreulem  15520  clim2div  16051  prodfmul  16052  prodmolem3  16093  sinhval  16315  coshval  16316  absefib  16359  efieq1re  16360  muldvds1  16443  muldvds2  16444  dvdsmulc  16446  dvdsmulcr  16448  dvdstr  16457  eulerthlem2  16952  oddprmdvds  17074  ablfacrp  20275  cncrng  21692  nmoleub2lem3  25429  cnlmod  25454  itg2mulc  26061  abssinper  26842  sinasin  27210  dchrabl  27574  bposlem6  27609  bposlem9  27612  2sqlem6  27743  rpvmasum2  27832  cncvcOLD  31178  ipasslem5  31430  ipasslem11  31435  dvasin  38602  facp2  43173  pellexlem2  43816  jm2.25  43985  expgrowth  45304  2zrngmsgrp  49319  nn0sumshdiglemA  49700