add4

Description: Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999) (Proof shortened by Andrew Salmon, 22-Oct-2011)

		Ref	Expression
	Assertion	add4	$⊢ ((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		add12	$⊢ (B \in ℂ \land C \in ℂ \land D \in ℂ) \to B + C + D = C + B + D$
2	1	3expb	$⊢ (B \in ℂ \land (C \in ℂ \land D \in ℂ)) \to B + C + D = C + B + D$
3	2	oveq2d	$⊢ (B \in ℂ \land (C \in ℂ \land D \in ℂ)) \to A + B + (C + D) = A + C + (B + D)$
4	3	adantll	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + B + (C + D) = A + C + (B + D)$
5		addcl	$⊢ (C \in ℂ \land D \in ℂ) \to C + D \in ℂ$
6		addass	$⊢ (A \in ℂ \land B \in ℂ \land C + D \in ℂ) \to A + B + C + D = A + B + (C + D)$
7	6	3expa	$⊢ ((A \in ℂ \land B \in ℂ) \land C + D \in ℂ) \to A + B + C + D = A + B + (C + D)$
8	5 7	sylan2	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + B + C + D = A + B + (C + D)$
9		addcl	$⊢ (B \in ℂ \land D \in ℂ) \to B + D \in ℂ$
10		addass	$⊢ (A \in ℂ \land C \in ℂ \land B + D \in ℂ) \to A + C + B + D = A + C + (B + D)$
11	10	3expa	$⊢ ((A \in ℂ \land C \in ℂ) \land B + D \in ℂ) \to A + C + B + D = A + C + (B + D)$
12	9 11	sylan2	$⊢ ((A \in ℂ \land C \in ℂ) \land (B \in ℂ \land D \in ℂ)) \to A + C + B + D = A + C + (B + D)$
13	12	an4s	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + C + B + D = A + C + (B + D)$
14	4 8 13	3eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + B + C + D = A + C + B + D$

Metamath Proof Explorer