Metamath Proof Explorer

Theorem mulneg2i

Description: Product with negative is negative of product. (Contributed by NM, 31-Jul-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses mulm1.1 A
mulneg.2 B
Assertion mulneg2i A B = A B


Step Hyp Ref Expression
1 mulm1.1 A
2 mulneg.2 B
3 mulneg2 A B A B = A B
4 1 2 3 mp2an A B = A B