Theorem joinlmuladdmuli

Description: Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019)

	Ref	Expression
Hypotheses	joinlmuladdmuli.1	$$⊢A\in ℂ$$
	joinlmuladdmuli.2	$$⊢B\in ℂ$$
	joinlmuladdmuli.3	$$⊢C\in ℂ$$
	joinlmuladdmuli.4	$$⊢AB+CB=D$$
Assertion	joinlmuladdmuli	$$⊢\left(A+C\right)B=D$$

Proof

Step	Hyp	Ref	Expression
1		joinlmuladdmuli.1	$$⊢A\in ℂ$$
2		joinlmuladdmuli.2	$$⊢B\in ℂ$$
3		joinlmuladdmuli.3	$$⊢C\in ℂ$$
4		joinlmuladdmuli.4	$$⊢AB+CB=D$$
5	1	a1i	$$⊢\top \to A\in ℂ$$
6	2	a1i	$$⊢\top \to B\in ℂ$$
7	3	a1i	$$⊢\top \to C\in ℂ$$
8	4	a1i	$$⊢\top \to AB+CB=D$$
9	5 6 7 8	joinlmuladdmuld	$$⊢\top \to \left(A+C\right)B=D$$
10	9	mptru	$$⊢\left(A+C\right)B=D$$