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 7905 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1233 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1348 ∈ wcel 2141 (class class class)co 5853 ℂcc 7772 · cmul 7779 |
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 7877 |
This theorem depends on definitions: df-bi 116 df-3an 975 |
This theorem is referenced by: ltmul1 8511 recexap 8571 mulap0 8572 mulcanapd 8579 receuap 8587 divmulasscomap 8613 divdivdivap 8630 divmuleqap 8634 conjmulap 8646 apmul1 8705 qapne 9598 modqmul1 10333 modqdi 10348 expadd 10518 mulbinom2 10592 binom3 10593 faclbnd 10675 faclbnd6 10678 bcm1k 10694 bcp1nk 10696 bcval5 10697 crre 10821 remullem 10835 resqrexlemcalc1 10978 resqrexlemnm 10982 amgm2 11082 binomlem 11446 geo2sum 11477 mertenslemi1 11498 clim2prod 11502 sinadd 11699 tanaddap 11702 dvdsmulcr 11783 dvdsmulgcd 11980 qredeq 12050 2sqpwodd 12130 pcaddlem 12292 prmpwdvds 12307 dvexp 13469 tangtx 13553 cxpmul 13627 binom4 13691 lgsneg 13719 2sqlem3 13747 |
Copyright terms: Public domain | W3C validator |