Metamath Proof Explorer

Theorem subdid

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 subdid φ A B C = A B A C


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