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 φABC=ABAC

Proof

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