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 7719 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1201 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1316 ∈ wcel 1465 (class class class)co 5742 ℂcc 7586 · cmul 7593 |
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 7691 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: ltmul1 8322 recexap 8382 mulap0 8383 mulcanapd 8390 receuap 8398 divmulasscomap 8424 divdivdivap 8441 divmuleqap 8445 conjmulap 8457 apmul1 8516 qapne 9399 modqmul1 10118 modqdi 10133 expadd 10303 mulbinom2 10376 binom3 10377 faclbnd 10455 faclbnd6 10458 bcm1k 10474 bcp1nk 10476 bcval5 10477 crre 10597 remullem 10611 resqrexlemcalc1 10754 resqrexlemnm 10758 amgm2 10858 binomlem 11220 geo2sum 11251 mertenslemi1 11272 sinadd 11370 tanaddap 11373 dvdsmulcr 11450 dvdsmulgcd 11640 qredeq 11704 2sqpwodd 11781 dvexp 12771 tangtx 12846 |
Copyright terms: Public domain | W3C validator |