Step |
Hyp |
Ref |
Expression |
1 |
|
ax-his1 |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ด ยทih ๐ต ) = ( โ โ ( ๐ต ยทih ๐ด ) ) ) |
2 |
1
|
fveq2d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( abs โ ( ๐ด ยทih ๐ต ) ) = ( abs โ ( โ โ ( ๐ต ยทih ๐ด ) ) ) ) |
3 |
|
hicl |
โข ( ( ๐ต โ โ โง ๐ด โ โ ) โ ( ๐ต ยทih ๐ด ) โ โ ) |
4 |
3
|
ancoms |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ต ยทih ๐ด ) โ โ ) |
5 |
4
|
abscjd |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( abs โ ( โ โ ( ๐ต ยทih ๐ด ) ) ) = ( abs โ ( ๐ต ยทih ๐ด ) ) ) |
6 |
2 5
|
eqtrd |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( abs โ ( ๐ด ยทih ๐ต ) ) = ( abs โ ( ๐ต ยทih ๐ด ) ) ) |