| 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 11243 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | |
| 5 | 1, 2, 3, 4 | mp3an 1463 | 1 ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 · cmul 11160 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulass 11221 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: 8th4div3 12486 numma 12777 decbin0 12873 sq4e2t8 14238 3dec 14305 faclbnd4lem1 14332 ef01bndlem 16220 3dvdsdec 16369 3dvds2dec 16370 dec5dvds 17102 karatsuba 17121 sincos4thpi 26555 sincos6thpi 26558 ang180lem2 26853 ang180lem3 26854 asin1 26937 efiatan2 26960 2efiatan 26961 log2cnv 26987 log2ublem2 26990 log2ublem3 26991 log2ub 26992 bclbnd 27324 bposlem8 27335 2lgsoddprmlem3d 27457 ax5seglem7 28950 ipasslem10 30858 siilem1 30870 normlem0 31128 normlem9 31137 bcseqi 31139 polid2i 31176 dfdec100 32832 dpmul100 32879 dpmul1000 32881 dpexpp1 32890 dpmul4 32896 quad3 35675 iexpire 35735 mulassnni 41987 sn-1ticom 42464 sn-0tie0 42469 sn-inelr 42497 fourierswlem 46245 fouriersw 46246 41prothprm 47606 tgoldbachlt 47803 |
| Copyright terms: Public domain | W3C validator |