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	$$⊢\phi \to A\in ℂ$$
	subadd4b.2	$$⊢\phi \to B\in ℂ$$
	subadd4b.3	$$⊢\phi \to C\in ℂ$$
	subadd4b.4	$$⊢\phi \to D\in ℂ$$
Assertion	subadd4b	$$⊢\phi \to \left(A-B\right)+C-D=\left(A-D\right)+C-B$$

Proof

Step	Hyp	Ref	Expression
1		subadd4b.1	$$⊢\phi \to A\in ℂ$$
2		subadd4b.2	$$⊢\phi \to B\in ℂ$$
3		subadd4b.3	$$⊢\phi \to C\in ℂ$$
4		subadd4b.4	$$⊢\phi \to D\in ℂ$$
5	1 2 4 3	subadd4d	$$⊢\phi \to A-B-\left(D-C\right)=A+C-\left(B+D\right)$$
6	1 2	subcld	$$⊢\phi \to A-B\in ℂ$$
7	6 4 3	subsub2d	$$⊢\phi \to A-B-\left(D-C\right)=\left(A-B\right)+C-D$$
8	2 4	addcomd	$$⊢\phi \to B+D=D+B$$
9	8	oveq2d	$$⊢\phi \to A+C-\left(B+D\right)=A+C-\left(D+B\right)$$
10	1 3 4 2	addsub4d	$$⊢\phi \to A+C-\left(D+B\right)=\left(A-D\right)+C-B$$
11	9 10	eqtrd	$$⊢\phi \to A+C-\left(B+D\right)=\left(A-D\right)+C-B$$
12	5 7 11	3eqtr3d	$$⊢\phi \to \left(A-B\right)+C-D=\left(A-D\right)+C-B$$