Metamath Proof Explorer
Description: Alias for ax-mulass , for naming consistency with mulassi .
(Contributed by NM, 10-Mar-2008)
|
|
Ref |
Expression |
|
Assertion |
mulass |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ax-mulass |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) ) |