Theorem mulass 11183

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   · cmul 11100

This theorem was proved from axioms:  ax-mulass 11161

This theorem is referenced by:  mulrid  11201  mulassi  11215  mulassd  11227  mul12  11370  mul32  11371  mul31  11372  mul4  11373  00id  11380  divass  11885  cju  12209  div4p1lem1div2  12494  xmulasslem3  13307  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  16205  coshval  16206  absefib  16249  efieq1re  16250  muldvds1  16333  muldvds2  16334  dvdsmulc  16336  dvdsmulcr  16338  dvdstr  16347  eulerthlem2  16836  oddprmdvds  16958  ablfacrp  20133  cncrng  21543  nmoleub2lem3  25274  cnlmod  25299  itg2mulc  25906  abssinper  26686  sinasin  27054  dchrabl  27418  bposlem6  27453  bposlem9  27456  2sqlem6  27587  rpvmasum2  27676  cncvcOLD  30935  ipasslem5  31187  ipasslem11  31192  dvasin  38355  facp2  42910  pellexlem2  43557  jm2.25  43726  expgrowth  45045  2zrngmsgrp  49018  nn0sumshdiglemA  49399