Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | addcld.1 | โข ( ๐ โ ๐ด โ โ ) | |
addcld.2 | โข ( ๐ โ ๐ต โ โ ) | ||
addassd.3 | โข ( ๐ โ ๐ถ โ โ ) | ||
Assertion | mulassd | โข ( ๐ โ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | โข ( ๐ โ ๐ด โ โ ) | |
2 | addcld.2 | โข ( ๐ โ ๐ต โ โ ) | |
3 | addassd.3 | โข ( ๐ โ ๐ถ โ โ ) | |
4 | mulass | โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) ) | |
5 | 1 2 3 4 | syl3anc | โข ( ๐ โ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) ) |