Step | Hyp | Ref
| Expression |
1 | | mulcom 11144 |
. . . 4
โข ((๐ถ โ โ โง ๐ท โ โ) โ (๐ถ ยท ๐ท) = (๐ท ยท ๐ถ)) |
2 | 1 | adantl 483 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ถ ยท ๐ท) = (๐ท ยท ๐ถ)) |
3 | 2 | oveq2d 7378 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท)) = ((๐ด ยท ๐ต) ยท (๐ท ยท ๐ถ))) |
4 | | mul4 11330 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ท โ โ โง ๐ถ โ โ)) โ ((๐ด ยท ๐ต) ยท (๐ท ยท ๐ถ)) = ((๐ด ยท ๐ท) ยท (๐ต ยท ๐ถ))) |
5 | 4 | ancom2s 649 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ต) ยท (๐ท ยท ๐ถ)) = ((๐ด ยท ๐ท) ยท (๐ต ยท ๐ถ))) |
6 | | simplr 768 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ๐ต โ
โ) |
7 | | simprl 770 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ๐ถ โ
โ) |
8 | 6, 7 | mulcomd 11183 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ถ) = (๐ถ ยท ๐ต)) |
9 | 8 | oveq2d 7378 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ท) ยท (๐ต ยท ๐ถ)) = ((๐ด ยท ๐ท) ยท (๐ถ ยท ๐ต))) |
10 | 3, 5, 9 | 3eqtrd 2781 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท)) = ((๐ด ยท ๐ท) ยท (๐ถ ยท ๐ต))) |