Theorem mulass 11126

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   · cmul 11043

This theorem was proved from axioms:  ax-mulass 11104

This theorem is referenced by:  mulrid  11142  mulassi  11156  mulassd  11168  mul12  11311  mul32  11312  mul31  11313  mul4  11314  00id  11321  divass  11827  cju  12155  div4p1lem1div2  12432  xmulasslem3  13238  mulbinom2  14185  sqoddm1div8  14205  faclbnd5  14260  bcval5  14280  remim  15079  imval2  15113  01sqrexlem7  15210  sqrtneglem  15228  sqreulem  15322  clim2div  15854  prodfmul  15855  prodmolem3  15898  sinhval  16121  coshval  16122  absefib  16165  efieq1re  16166  muldvds1  16249  muldvds2  16250  dvdsmulc  16252  dvdsmulcr  16254  dvdstr  16263  eulerthlem2  16752  oddprmdvds  16874  ablfacrp  20043  cncrng  21373  nmoleub2lem3  25082  cnlmod  25107  itg2mulc  25714  abssinper  26485  sinasin  26853  dchrabl  27217  bposlem6  27252  bposlem9  27255  2sqlem6  27386  rpvmasum2  27475  cncvcOLD  30654  ipasslem5  30906  ipasslem11  30911  dvasin  38025  facp2  42582  pellexlem2  43258  jm2.25  43427  expgrowth  44762  2zrngmsgrp  48729  nn0sumshdiglemA  49095