Metamath Proof Explorer

Theorem add42

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

Ref Expression
Assertion add42 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ→A+B+C+D=A+C+D+B

Proof

Step Hyp Ref Expression
1 add4 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ→A+B+C+D=A+C+B+D
2 addcom ⊢B∈ℂ∧D∈ℂ→B+D=D+B
3 2 ad2ant2l ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ→B+D=D+B
4 3 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ→A+C+B+D=A+C+D+B
5 1 4 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧D∈ℂ→A+B+C+D=A+C+D+B