Metamath Proof Explorer

Theorem subdird

Description: Distribution of multiplication over subtraction. Theorem I.5 of Apostol p. 18. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses mulm1d.1 φ A
mulnegd.2 φ B
subdid.3 φ C
Assertion subdird φ A B C = A C B C


Step Hyp Ref Expression
1 mulm1d.1 φ A
2 mulnegd.2 φ B
3 subdid.3 φ C
4 subdir A B C A B C = A C B C
5 1 2 3 4 syl3anc φ A B C = A C B C