Theorem mulass 11212

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

Assertion

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

Proof of Theorem mulass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  (class class class)co 7413  ℂcc 11122   · cmul 11129

This proof depends on axioms:  ax-mulass 11190

This theorem is used by:  mulrid  11230  mulassi  11244  mulassd  11256  mul12  11399  mul32  11400  mul31  11401  mul4  11402  00id  11409  divass  11914  cju  12238  div4p1lem1div2  12523  xmulasslem3  13338  mulbinom2  14287  sqoddm1div8  14307  faclbnd5  14362  bcval5  14382  remim  15204  imval2  15238  01sqrexlem7  15335  sqrtneglem  15353  sqreulem  15447  clim2div  15978  prodfmul  15979  prodmolem3  16020  sinhval  16242  coshval  16243  absefib  16286  efieq1re  16287  muldvds1  16370  muldvds2  16371  dvdsmulc  16373  dvdsmulcr  16375  dvdstr  16384  eulerthlem2  16873  oddprmdvds  16995  ablfacrp  20195  cncrng  21606  nmoleub2lem3  25343  cnlmod  25368  itg2mulc  25975  abssinper  26758  sinasin  27126  dchrabl  27490  bposlem6  27525  bposlem9  27528  2sqlem6  27659  rpvmasum2  27748  cncvcOLD  31064  ipasslem5  31316  ipasslem11  31321  dvasin  38453  facp2  43009  pellexlem2  43671  jm2.25  43840  expgrowth  45159  2zrngmsgrp  49168  nn0sumshdiglemA  49549