Metamath Proof Explorer

Theorem mulneg1d

Description: Product with negative is negative of product. Theorem I.12 of Apostol p. 18. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses mulm1d.1 φ A
mulnegd.2 φ B
Assertion mulneg1d φ A B = A B


Step Hyp Ref Expression
1 mulm1d.1 φ A
2 mulnegd.2 φ B
3 mulneg1 A B A B = A B
4 1 2 3 syl2anc φ A B = A B