Theorem mulass 11327

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

Assertion

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

Proof of Theorem mulass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237   · cmul 11244

This proof depends on axioms:  ax-mulass 11305

This theorem is used by:  mulrid  11345  mulassi  11359  mulassd  11371  mul12  11514  mul32  11515  mul31  11516  mul4  11517  00id  11524  divass  12032  cju  12356  div4p1lem1div2  12641  xmulasslem3  13456  mulbinom2  14408  sqoddm1div8  14428  faclbnd5  14483  bcval5  14503  remim  15327  imval2  15361  01sqrexlem7  15458  sqrtneglem  15476  sqreulem  15571  clim2div  16102  prodfmul  16103  prodmolem3  16144  sinhval  16366  coshval  16367  absefib  16410  efieq1re  16411  muldvds1  16494  muldvds2  16495  dvdsmulc  16497  dvdsmulcr  16499  dvdstr  16508  eulerthlem2  17003  oddprmdvds  17125  ablfacrp  20333  cncrng  21751  nmoleub2lem3  25491  cnlmod  25516  itg2mulc  26123  abssinper  26906  sinasin  27274  dchrabl  27638  bposlem6  27673  bposlem9  27676  2sqlem6  27807  rpvmasum2  27896  cncvcOLD  31242  ipasslem5  31494  ipasslem11  31499  dvasin  38890  facp2  43459  pellexlem2  44103  jm2.25  44272  expgrowth  45580  2zrngmsgrp  49623  nn0sumshdiglemA  50062