Description: MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | int-mulcomd.1 | โข ( ๐ โ ๐ต โ โ ) | |
int-mulcomd.2 | โข ( ๐ โ ๐ถ โ โ ) | ||
int-mulcomd.3 | โข ( ๐ โ ๐ด = ๐ต ) | ||
Assertion | int-mulcomd | โข ( ๐ โ ( ๐ต ยท ๐ถ ) = ( ๐ถ ยท ๐ด ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | int-mulcomd.1 | โข ( ๐ โ ๐ต โ โ ) | |
2 | int-mulcomd.2 | โข ( ๐ โ ๐ถ โ โ ) | |
3 | int-mulcomd.3 | โข ( ๐ โ ๐ด = ๐ต ) | |
4 | 1 | recnd | โข ( ๐ โ ๐ต โ โ ) |
5 | 2 | recnd | โข ( ๐ โ ๐ถ โ โ ) |
6 | 4 5 | mulcomd | โข ( ๐ โ ( ๐ต ยท ๐ถ ) = ( ๐ถ ยท ๐ต ) ) |
7 | 3 | eqcomd | โข ( ๐ โ ๐ต = ๐ด ) |
8 | 7 | oveq2d | โข ( ๐ โ ( ๐ถ ยท ๐ต ) = ( ๐ถ ยท ๐ด ) ) |
9 | 6 8 | eqtrd | โข ( ๐ โ ( ๐ต ยท ๐ถ ) = ( ๐ถ ยท ๐ด ) ) |