Theorem subadd4b

Description: Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		subadd4b.1	|- ( ph -> A e. CC )
2		subadd4b.2	|- ( ph -> B e. CC )
3		subadd4b.3	|- ( ph -> C e. CC )
4		subadd4b.4	|- ( ph -> D e. CC )
5	1 2 4 3	subadd4d	|- ( ph -> ( ( A - B ) - ( D - C ) ) = ( ( A + C ) - ( B + D ) ) )
6	1 2	subcld	|- ( ph -> ( A - B ) e. CC )
7	6 4 3	subsub2d	|- ( ph -> ( ( A - B ) - ( D - C ) ) = ( ( A - B ) + ( C - D ) ) )
8	2 4	addcomd	|- ( ph -> ( B + D ) = ( D + B ) )
9	8	oveq2d	|- ( ph -> ( ( A + C ) - ( B + D ) ) = ( ( A + C ) - ( D + B ) ) )
10	1 3 4 2	addsub4d	|- ( ph -> ( ( A + C ) - ( D + B ) ) = ( ( A - D ) + ( C - B ) ) )
11	9 10	eqtrd	|- ( ph -> ( ( A + C ) - ( B + D ) ) = ( ( A - D ) + ( C - B ) ) )
12	5 7 11	3eqtr3d	|- ( ph -> ( ( A - B ) + ( C - D ) ) = ( ( A - D ) + ( C - B ) ) )