![]() |
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 7941 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1238 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ∈ wcel 2148 (class class class)co 5874 ℂcc 7808 · cmul 7815 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-mulass 7913 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: ltmul1 8548 recexap 8609 mulap0 8610 mulcanapd 8617 receuap 8625 divmulasscomap 8652 divdivdivap 8669 divmuleqap 8673 conjmulap 8685 apmul1 8744 qapne 9638 modqmul1 10376 modqdi 10391 expadd 10561 mulbinom2 10636 binom3 10637 faclbnd 10720 faclbnd6 10723 bcm1k 10739 bcp1nk 10741 bcval5 10742 crre 10865 remullem 10879 resqrexlemcalc1 11022 resqrexlemnm 11026 amgm2 11126 binomlem 11490 geo2sum 11521 mertenslemi1 11542 clim2prod 11546 sinadd 11743 tanaddap 11746 dvdsmulcr 11827 dvdsmulgcd 12025 qredeq 12095 2sqpwodd 12175 pcaddlem 12337 prmpwdvds 12352 dvexp 14111 tangtx 14195 cxpmul 14269 binom4 14333 lgsneg 14361 lgseisenlem1 14386 lgseisenlem2 14387 2lgsoddprmlem2 14390 2sqlem3 14400 |
Copyright terms: Public domain | W3C validator |