Step |
Hyp |
Ref |
Expression |
1 |
|
negcl |
โข ( ๐ต โ โ โ - ๐ต โ โ ) |
2 |
|
mulneg12 |
โข ( ( ๐ด โ โ โง - ๐ต โ โ ) โ ( - ๐ด ยท - ๐ต ) = ( ๐ด ยท - - ๐ต ) ) |
3 |
1 2
|
sylan2 |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( - ๐ด ยท - ๐ต ) = ( ๐ด ยท - - ๐ต ) ) |
4 |
|
negneg |
โข ( ๐ต โ โ โ - - ๐ต = ๐ต ) |
5 |
4
|
adantl |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ - - ๐ต = ๐ต ) |
6 |
5
|
oveq2d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ด ยท - - ๐ต ) = ( ๐ด ยท ๐ต ) ) |
7 |
3 6
|
eqtrd |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( - ๐ด ยท - ๐ต ) = ( ๐ด ยท ๐ต ) ) |