Metamath Proof Explorer


Theorem mulneg12

Description: Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004)

Ref Expression
Assertion mulneg12 A B A B = A B

Proof

Step Hyp Ref Expression
1 mulneg1 A B A B = A B
2 mulneg2 A B A B = A B
3 1 2 eqtr4d A B A B = A B