Metamath Proof Explorer


Theorem submuladdmuld

Description: Transformation of a sum of a product of a difference and a product with the subtrahend of the difference. (Contributed by AV, 2-Feb-2023)

Ref Expression
Hypotheses submuladdmuld.a φ A
submuladdmuld.b φ B
submuladdmuld.c φ C
submuladdmuld.d φ D
Assertion submuladdmuld φ A B C + B D = A C + B D C

Proof

Step Hyp Ref Expression
1 submuladdmuld.a φ A
2 submuladdmuld.b φ B
3 submuladdmuld.c φ C
4 submuladdmuld.d φ D
5 1 2 3 subdird φ A B C = A C B C
6 5 oveq1d φ A B C + B D = A C - B C + B D
7 1 3 mulcld φ A C
8 2 3 mulcld φ B C
9 2 4 mulcld φ B D
10 7 8 9 subadd23d φ A C - B C + B D = A C + B D - B C
11 2 4 3 subdid φ B D C = B D B C
12 11 eqcomd φ B D B C = B D C
13 12 oveq2d φ A C + B D - B C = A C + B D C
14 6 10 13 3eqtrd φ A B C + B D = A C + B D C