Metamath Proof Explorer


Theorem muladdd

Description: Product of two sums. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses mulm1d.1 φ A
mulnegd.2 φ B
subdid.3 φ C
muladdd.4 φ D
Assertion muladdd φ A + B C + D = A C + D B + A D + C B

Proof

Step Hyp Ref Expression
1 mulm1d.1 φ A
2 mulnegd.2 φ B
3 subdid.3 φ C
4 muladdd.4 φ D
5 muladd A B C D A + B C + D = A C + D B + A D + C B
6 1 2 3 4 5 syl22anc φ A + B C + D = A C + D B + A D + C B