Theorem mulass 10606

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  (class class class)co 7137  ℂcc 10516   · cmul 10523

This theorem was proved from axioms:  ax-mulass 10584

This theorem is referenced by:  mulid1  10620  mulassi  10633  mulassd  10645  mul12  10786  mul32  10787  mul31  10788  mul4  10789  00id  10796  divass  11297  cju  11615  div4p1lem1div2  11874  xmulasslem3  12661  mulbinom2  13569  sqoddm1div8  13589  faclbnd5  13643  bcval5  13663  remim  14456  imval2  14490  sqrlem7  14588  sqrtneglem  14606  sqreulem  14699  clim2div  15225  prodfmul  15226  prodmolem3  15267  sinhval  15487  coshval  15488  absefib  15531  efieq1re  15532  muldvds1  15614  muldvds2  15615  dvdsmulc  15617  dvdsmulcr  15619  dvdstr  15626  eulerthlem2  16097  oddprmdvds  16217  ablfacrp  19166  cncrng  20544  nmoleub2lem3  23697  cnlmod  23722  itg2mulc  24326  abssinper  25087  sinasin  25448  dchrabl  25811  bposlem6  25846  bposlem9  25849  2sqlem6  25980  rpvmasum2  26069  cncvcOLD  28339  ipasslem5  28591  ipasslem11  28596  dvasin  35005  fac2xp3  39164  facp2  39165  pellexlem2  39514  jm2.25  39683  expgrowth  40752  2zrngmsgrp  44298  nn0sumshdiglemA  44759