Metamath Proof Explorer


Theorem int-mulcomd

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 ( ๐œ‘ โ†’ ( ๐ต ยท ๐ถ ) = ( ๐ถ ยท ๐ด ) )

Proof

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