sub4

Description: Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007)

		Ref	Expression
	Assertion	sub4	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A - B - (C - D) = A - C - (B - D)$

Step	Hyp	Ref	Expression
1		addcom	$⊢ (B \in ℂ \land C \in ℂ) \to B + C = C + B$
2	1	ad2ant2lr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B + C = C + B$
3	2	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + D - (B + C) = A + D - (C + B)$
4		subadd4	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A - B - (C - D) = A + D - (B + C)$
5		subadd4	$⊢ ((A \in ℂ \land C \in ℂ) \land (B \in ℂ \land D \in ℂ)) \to A - C - (B - D) = A + D - (C + B)$
6	5	an4s	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A - C - (B - D) = A + D - (C + B)$
7	3 4 6	3eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A - B - (C - D) = A - C - (B - D)$

Metamath Proof Explorer