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 e. CC
	joinlmuladdmuli.2	|- B e. CC
	joinlmuladdmuli.3	|- C e. CC
	joinlmuladdmuli.4	|- ( ( A x. B ) + ( C x. B ) ) = D
Assertion	joinlmuladdmuli	|- ( ( A + C ) x. B ) = D

Proof

Step	Hyp	Ref	Expression
1		joinlmuladdmuli.1	|- A e. CC
2		joinlmuladdmuli.2	|- B e. CC
3		joinlmuladdmuli.3	|- C e. CC
4		joinlmuladdmuli.4	|- ( ( A x. B ) + ( C x. B ) ) = D
5	1	a1i	|- ( T. -> A e. CC )
6	2	a1i	|- ( T. -> B e. CC )
7	3	a1i	|- ( T. -> C e. CC )
8	4	a1i	|- ( T. -> ( ( A x. B ) + ( C x. B ) ) = D )
9	5 6 7 8	joinlmuladdmuld	|- ( T. -> ( ( A + C ) x. B ) = D )
10	9	mptru	|- ( ( A + C ) x. B ) = D