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 10613 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1452 | 1 ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 · cmul 10530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulass 10591 |
This theorem depends on definitions: df-bi 208 df-an 397 df-3an 1081 |
This theorem is referenced by: 8th4div3 11845 numma 12130 decbin0 12226 sq4e2t8 13550 3dec 13614 faclbnd4lem1 13641 ef01bndlem 15525 3dvdsdec 15669 3dvds2dec 15670 dec5dvds 16388 karatsuba 16408 sincos4thpi 25026 sincos6thpi 25028 ang180lem2 25315 ang180lem3 25316 asin1 25399 efiatan2 25422 2efiatan 25423 log2cnv 25449 log2ublem2 25452 log2ublem3 25453 log2ub 25454 bclbnd 25783 bposlem8 25794 2lgsoddprmlem3d 25916 ax5seglem7 26648 ipasslem10 28543 siilem1 28555 normlem0 28813 normlem9 28822 bcseqi 28824 polid2i 28861 dfdec100 30473 dpmul100 30500 dpmul1000 30502 dpexpp1 30511 dpmul4 30517 quad3 32810 iexpire 32864 fourierswlem 42392 fouriersw 42393 41prothprm 43661 tgoldbachlt 43858 |
Copyright terms: Public domain | W3C validator |