Metamath Proof Explorer


Theorem add42

Description: Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005)

Ref Expression
Assertion add42 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) + ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( 𝐷 + 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 add4 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) + ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( 𝐵 + 𝐷 ) ) )
2 addcom ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐵 + 𝐷 ) = ( 𝐷 + 𝐵 ) )
3 2 ad2ant2l ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐵 + 𝐷 ) = ( 𝐷 + 𝐵 ) )
4 3 oveq2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐶 ) + ( 𝐵 + 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( 𝐷 + 𝐵 ) ) )
5 1 4 eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) + ( 𝐶 + 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( 𝐷 + 𝐵 ) ) )