Theorem mulass 11184

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  (class class class)co 7408  ℂcc 11094   · cmul 11101

This theorem was proved from axioms:  ax-mulass 11162

This theorem is referenced by:  mulrid  11202  mulassi  11216  mulassd  11228  mul12  11371  mul32  11372  mul31  11373  mul4  11374  00id  11381  divass  11886  cju  12210  div4p1lem1div2  12495  xmulasslem3  13308  mulbinom2  14255  sqoddm1div8  14275  faclbnd5  14330  bcval5  14350  remim  15164  imval2  15198  01sqrexlem7  15295  sqrtneglem  15313  sqreulem  15407  clim2div  15939  prodfmul  15940  prodmolem3  15983  sinhval  16206  coshval  16207  absefib  16250  efieq1re  16251  muldvds1  16334  muldvds2  16335  dvdsmulc  16337  dvdsmulcr  16339  dvdstr  16348  eulerthlem2  16837  oddprmdvds  16959  ablfacrp  20134  cncrng  21508  nmoleub2lem3  25239  cnlmod  25264  itg2mulc  25871  abssinper  26648  sinasin  27016  dchrabl  27380  bposlem6  27415  bposlem9  27418  2sqlem6  27549  rpvmasum2  27638  cncvcOLD  30872  ipasslem5  31124  ipasslem11  31129  dvasin  38238  facp2  42795  pellexlem2  43444  jm2.25  43613  expgrowth  44932  2zrngmsgrp  48902  nn0sumshdiglemA  49279