Theorem mulass 9969

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1036   = wceq 1480   ∈ wcel 1992  (class class class)co 6605  ℂcc 9879   · cmul 9886

This theorem was proved from axioms:  ax-mulass 9947

This theorem is referenced by:  mulid1  9982  mulassi  9994  mulassd  10008  mul12  10147  mul32  10148  mul31  10149  mul4  10150  00id  10156  divass  10648  cju  10961  div4p1lem1div2  11232  xmulasslem3  12056  mulbinom2  12921  sqoddm1div8  12965  faclbnd5  13022  bcval5  13042  remim  13786  imval2  13820  sqrlem7  13918  sqrtneglem  13936  sqreulem  14028  clim2div  14541  prodfmul  14542  prodmolem3  14583  sinhval  14804  coshval  14805  absefib  14848  efieq1re  14849  muldvds1  14925  muldvds2  14926  dvdsmulc  14928  dvdsmulcr  14930  dvdstr  14937  eulerthlem2  15406  oddprmdvds  15526  ablfacrp  18381  cncrng  19681  nmoleub2lem3  22818  cnlmod  22843  itg2mulc  23415  abssinper  24169  sinasin  24511  dchrabl  24874  bposlem6  24909  bposlem9  24912  lgsdir  24952  lgsdi  24954  2sqlem6  25043  rpvmasum2  25096  cncvcOLD  27278  ipasslem5  27530  ipasslem11  27535  dvasin  33114  pellexlem2  36860  jm2.25  37032  expgrowth  38002  2zrngmsgrp  41208  nn0sumshdiglemA  41679