![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulassi | Structured version Visualization version GIF version |
Description: Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
axi.2 | ⊢ 𝐵 ∈ ℂ |
axi.3 | ⊢ 𝐶 ∈ ℂ |
Ref | Expression |
---|---|
mulassi | ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | axi.2 | . 2 ⊢ 𝐵 ∈ ℂ | |
3 | axi.3 | . 2 ⊢ 𝐶 ∈ ℂ | |
4 | mulass 10347 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1589 | 1 ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 ∈ wcel 2164 (class class class)co 6910 ℂcc 10257 · cmul 10264 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulass 10325 |
This theorem depends on definitions: df-bi 199 df-an 387 df-3an 1113 |
This theorem is referenced by: 8th4div3 11585 numma 11873 decbin0 11970 sq4e2t8 13263 3dec 13353 faclbnd4lem1 13380 ef01bndlem 15293 3dvdsdec 15437 3dvds2dec 15438 dec5dvds 16146 karatsuba 16166 sincos4thpi 24672 sincos6thpi 24674 ang180lem2 24957 ang180lem3 24958 asin1 25041 efiatan2 25064 2efiatan 25065 log2cnv 25091 log2ublem2 25094 log2ublem3 25095 log2ub 25096 bclbnd 25425 bposlem8 25436 2lgsoddprmlem3d 25558 ax5seglem7 26241 ipasslem10 28245 siilem1 28257 normlem0 28517 normlem9 28526 bcseqi 28528 polid2i 28565 dfdec100 30119 dpmul100 30146 dpmul1000 30148 dpexpp1 30157 dpmul4 30163 quad3 32104 iexpire 32159 fourierswlem 41235 fouriersw 41236 41prothprm 42380 tgoldbachlt 42548 |
Copyright terms: Public domain | W3C validator |