Theorem subeqxfrd

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

	Ref	Expression
Hypotheses	subeqxfrd.a	$$⊢\phi \to A\in ℂ$$
	subeqxfrd.b	$$⊢\phi \to B\in ℂ$$
	subeqxfrd.c	$$⊢\phi \to C\in ℂ$$
	subeqxfrd.d	$$⊢\phi \to D\in ℂ$$
	subeqxfrd.1	$$⊢\phi \to A-B=C-D$$
Assertion	subeqxfrd	$$⊢\phi \to A-C=B-D$$

Proof

Step	Hyp	Ref	Expression
1		subeqxfrd.a	$$⊢\phi \to A\in ℂ$$
2		subeqxfrd.b	$$⊢\phi \to B\in ℂ$$
3		subeqxfrd.c	$$⊢\phi \to C\in ℂ$$
4		subeqxfrd.d	$$⊢\phi \to D\in ℂ$$
5		subeqxfrd.1	$$⊢\phi \to A-B=C-D$$
6	5	oveq1d	$$⊢\phi \to \left(A-B\right)+B-C=\left(C-D\right)+B-C$$
7	1 2 3	npncand	$$⊢\phi \to \left(A-B\right)+B-C=A-C$$
8	3 4 2	npncan3d	$$⊢\phi \to \left(C-D\right)+B-C=B-D$$
9	6 7 8	3eqtr3d	$$⊢\phi \to A-C=B-D$$