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+BC+D=AC+DB+AD+CB

Proof

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