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	$$⊢\phi \to A\in ℂ$$
	subaddeqd.b	$$⊢\phi \to B\in ℂ$$
	subaddeqd.c	$$⊢\phi \to C\in ℂ$$
	subaddeqd.d	$$⊢\phi \to D\in ℂ$$
	subaddeqd.1	$$⊢\phi \to A+B=C+D$$
Assertion	subaddeqd	$$⊢\phi \to A-D=C-B$$

Proof

Step	Hyp	Ref	Expression
1		subaddeqd.a	$$⊢\phi \to A\in ℂ$$
2		subaddeqd.b	$$⊢\phi \to B\in ℂ$$
3		subaddeqd.c	$$⊢\phi \to C\in ℂ$$
4		subaddeqd.d	$$⊢\phi \to D\in ℂ$$
5		subaddeqd.1	$$⊢\phi \to A+B=C+D$$
6	5	oveq1d	$$⊢\phi \to A+B-\left(D+B\right)=C+D-\left(D+B\right)$$
7	3 4	addcomd	$$⊢\phi \to C+D=D+C$$
8	7	oveq1d	$$⊢\phi \to C+D-\left(D+B\right)=D+C-\left(D+B\right)$$
9	6 8	eqtrd	$$⊢\phi \to A+B-\left(D+B\right)=D+C-\left(D+B\right)$$
10	1 4 2	pnpcan2d	$$⊢\phi \to A+B-\left(D+B\right)=A-D$$
11	4 3 2	pnpcand	$$⊢\phi \to D+C-\left(D+B\right)=C-B$$
12	9 10 11	3eqtr3d	$$⊢\phi \to A-D=C-B$$