Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulassd | GIF version |
Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
addassd.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
Ref | Expression |
---|---|
mulassd | ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | addassd.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | mulass 7863 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1220 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1335 ∈ wcel 2128 (class class class)co 5824 ℂcc 7730 · cmul 7737 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-mulass 7835 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: ltmul1 8467 recexap 8527 mulap0 8528 mulcanapd 8535 receuap 8543 divmulasscomap 8569 divdivdivap 8586 divmuleqap 8590 conjmulap 8602 apmul1 8661 qapne 9548 modqmul1 10276 modqdi 10291 expadd 10461 mulbinom2 10534 binom3 10535 faclbnd 10615 faclbnd6 10618 bcm1k 10634 bcp1nk 10636 bcval5 10637 crre 10757 remullem 10771 resqrexlemcalc1 10914 resqrexlemnm 10918 amgm2 11018 binomlem 11380 geo2sum 11411 mertenslemi1 11432 clim2prod 11436 sinadd 11633 tanaddap 11636 dvdsmulcr 11717 dvdsmulgcd 11909 qredeq 11973 2sqpwodd 12051 dvexp 13086 tangtx 13170 cxpmul 13244 binom4 13307 |
Copyright terms: Public domain | W3C validator |