![]() |
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 7944 | . 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 5877 โcc 7811 ยท cmul 7818 |
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 7916 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: ltmul1 8551 recexap 8612 mulap0 8613 mulcanapd 8620 receuap 8628 divmulasscomap 8655 divdivdivap 8672 divmuleqap 8676 conjmulap 8688 apmul1 8747 qapne 9641 modqmul1 10379 modqdi 10394 expadd 10564 mulbinom2 10639 binom3 10640 faclbnd 10723 faclbnd6 10726 bcm1k 10742 bcp1nk 10744 bcval5 10745 crre 10868 remullem 10882 resqrexlemcalc1 11025 resqrexlemnm 11029 amgm2 11129 binomlem 11493 geo2sum 11524 mertenslemi1 11545 clim2prod 11549 sinadd 11746 tanaddap 11749 dvdsmulcr 11830 dvdsmulgcd 12028 qredeq 12098 2sqpwodd 12178 pcaddlem 12340 prmpwdvds 12355 dvexp 14260 tangtx 14344 cxpmul 14418 binom4 14482 lgsneg 14510 lgseisenlem1 14535 lgseisenlem2 14536 2lgsoddprmlem2 14539 2sqlem3 14549 |
Copyright terms: Public domain | W3C validator |