Theorem subeqxfrd

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

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

Proof

Step	Hyp	Ref	Expression
1		subeqxfrd.a	|- ( ph -> A e. CC )
2		subeqxfrd.b	|- ( ph -> B e. CC )
3		subeqxfrd.c	|- ( ph -> C e. CC )
4		subeqxfrd.d	|- ( ph -> D e. CC )
5		subeqxfrd.1	|- ( ph -> ( A - B ) = ( C - D ) )
6	5	oveq1d	|- ( ph -> ( ( A - B ) + ( B - C ) ) = ( ( C - D ) + ( B - C ) ) )
7	1 2 3	npncand	|- ( ph -> ( ( A - B ) + ( B - C ) ) = ( A - C ) )
8	3 4 2	npncan3d	|- ( ph -> ( ( C - D ) + ( B - C ) ) = ( B - D ) )
9	6 7 8	3eqtr3d	|- ( ph -> ( A - C ) = ( B - D ) )