Theorem subaddeqd

Description: Transfer two terms of a subtraction to an addition in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020)

	Ref	Expression
Hypotheses	subaddeqd.a	|- ( ph -> A e. CC )
	subaddeqd.b	|- ( ph -> B e. CC )
	subaddeqd.c	|- ( ph -> C e. CC )
	subaddeqd.d	|- ( ph -> D e. CC )
	subaddeqd.1	|- ( ph -> ( A + B ) = ( C + D ) )
Assertion	subaddeqd	|- ( ph -> ( A - D ) = ( C - B ) )

Proof

Step	Hyp	Ref	Expression
1		subaddeqd.a	|- ( ph -> A e. CC )
2		subaddeqd.b	|- ( ph -> B e. CC )
3		subaddeqd.c	|- ( ph -> C e. CC )
4		subaddeqd.d	|- ( ph -> D e. CC )
5		subaddeqd.1	|- ( ph -> ( A + B ) = ( C + D ) )
6	5	oveq1d	|- ( ph -> ( ( A + B ) - ( D + B ) ) = ( ( C + D ) - ( D + B ) ) )
7	3 4	addcomd	|- ( ph -> ( C + D ) = ( D + C ) )
8	7	oveq1d	|- ( ph -> ( ( C + D ) - ( D + B ) ) = ( ( D + C ) - ( D + B ) ) )
9	6 8	eqtrd	|- ( ph -> ( ( A + B ) - ( D + B ) ) = ( ( D + C ) - ( D + B ) ) )
10	1 4 2	pnpcan2d	|- ( ph -> ( ( A + B ) - ( D + B ) ) = ( A - D ) )
11	4 3 2	pnpcand	|- ( ph -> ( ( D + C ) - ( D + B ) ) = ( C - B ) )
12	9 10 11	3eqtr3d	|- ( ph -> ( A - D ) = ( C - B ) )