Metamath Proof Explorer


Theorem mulass

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 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) )