Theorem add42i

Description: Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999) (Proof shortened by OpenAI, 25-Mar-2020)

	Ref	Expression
Hypotheses	add.1	⊢ 𝐴 ∈ ℂ
	add.2	⊢ 𝐵 ∈ ℂ
	add.3	⊢ 𝐶 ∈ ℂ
	add4.4	⊢ 𝐷 ∈ ℂ
Assertion	add42i	⊢ ( ( 𝐴 + 𝐵 ) + ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( 𝐷 + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		add.1	⊢ 𝐴 ∈ ℂ
2		add.2	⊢ 𝐵 ∈ ℂ
3		add.3	⊢ 𝐶 ∈ ℂ
4		add4.4	⊢ 𝐷 ∈ ℂ
5		add42	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) + ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( 𝐷 + 𝐵 ) ) )
6	1 2 3 4 5	mp4an	⊢ ( ( 𝐴 + 𝐵 ) + ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( 𝐷 + 𝐵 ) )