Theorem mulassi 11249

Description: Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ
axi.3	⊢ 𝐶 ∈ ℂ

Assertion

Ref	Expression
mulassi	⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

Proof of Theorem mulassi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		axi.3	. 2 ⊢ 𝐶 ∈ ℂ
4		mulass 11220	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	mp3an 1458	1 ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

Syntax hints:   = wceq 1534   ∈ wcel 2099  (class class class)co 7414  ℂcc 11130   · cmul 11137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11198

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  8th4div3  12456  numma  12745  decbin0  12841  sq4e2t8  14188  3dec  14251  faclbnd4lem1  14278  ef01bndlem  16154  3dvdsdec  16302  3dvds2dec  16303  dec5dvds  17026  karatsuba  17046  sincos4thpi  26441  sincos6thpi  26443  ang180lem2  26735  ang180lem3  26736  asin1  26819  efiatan2  26842  2efiatan  26843  log2cnv  26869  log2ublem2  26872  log2ublem3  26873  log2ub  26874  bclbnd  27206  bposlem8  27217  2lgsoddprmlem3d  27339  ax5seglem7  28739  ipasslem10  30642  siilem1  30654  normlem0  30912  normlem9  30921  bcseqi  30923  polid2i  30960  dfdec100  32587  dpmul100  32614  dpmul1000  32616  dpexpp1  32625  dpmul4  32631  quad3  35268  iexpire  35323  mulassnni  41451  sn-1ticom  41983  sn-0tie0  41988  sn-inelr  42014  fourierswlem  45612  fouriersw  45613  41prothprm  46953  tgoldbachlt  47150

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »