Theorem joinlmulsubmuld

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

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

Proof

Step	Hyp	Ref	Expression
1		joinlmulsubmuld.1	|- ( ph -> A e. CC )
2		joinlmulsubmuld.2	|- ( ph -> B e. CC )
3		joinlmulsubmuld.3	|- ( ph -> C e. CC )
4		joinlmulsubmuld.4	|- ( ph -> ( ( A x. B ) - ( C x. B ) ) = D )
5	1 3 2	subdird	|- ( ph -> ( ( A - C ) x. B ) = ( ( A x. B ) - ( C x. B ) ) )
6	5 4	eqtrd	|- ( ph -> ( ( A - C ) x. B ) = D )