Theorem joinlmulsubmuli

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

	Ref	Expression
Hypotheses	joinlmulsubmuli.1	|- A e. CC
	joinlmulsubmuli.2	|- B e. CC
	joinlmulsubmuli.3	|- C e. CC
	joinlmulsubmuli.4	|- ( ( A x. B ) - ( C x. B ) ) = D
Assertion	joinlmulsubmuli	|- ( ( A - C ) x. B ) = D

Proof

Step	Hyp	Ref	Expression
1		joinlmulsubmuli.1	|- A e. CC
2		joinlmulsubmuli.2	|- B e. CC
3		joinlmulsubmuli.3	|- C e. CC
4		joinlmulsubmuli.4	|- ( ( A x. B ) - ( C x. B ) ) = D
5	1 3 2	subdiri	|- ( ( A - C ) x. B ) = ( ( A x. B ) - ( C x. B ) )
6	5 4	eqtri	|- ( ( A - C ) x. B ) = D