# Metamath Proof Explorer

## Theorem 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 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{B}+{C}+{D}={A}+{C}+{B}+{D}$

### Proof

Step Hyp Ref Expression
1 add12 ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\wedge {D}\in ℂ\right)\to {B}+{C}+{D}={C}+{B}+{D}$
2 1 3expb ${⊢}\left({B}\in ℂ\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {B}+{C}+{D}={C}+{B}+{D}$
3 2 oveq2d ${⊢}\left({B}\in ℂ\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{B}+\left({C}+{D}\right)={A}+{C}+\left({B}+{D}\right)$
4 3 adantll ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{B}+\left({C}+{D}\right)={A}+{C}+\left({B}+{D}\right)$
5 addcl ${⊢}\left({C}\in ℂ\wedge {D}\in ℂ\right)\to {C}+{D}\in ℂ$
6 addass ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}+{D}\in ℂ\right)\to {A}+{B}+{C}+{D}={A}+{B}+\left({C}+{D}\right)$
7 6 3expa ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge {C}+{D}\in ℂ\right)\to {A}+{B}+{C}+{D}={A}+{B}+\left({C}+{D}\right)$
8 5 7 sylan2 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{B}+{C}+{D}={A}+{B}+\left({C}+{D}\right)$
9 addcl ${⊢}\left({B}\in ℂ\wedge {D}\in ℂ\right)\to {B}+{D}\in ℂ$
10 addass ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\wedge {B}+{D}\in ℂ\right)\to {A}+{C}+{B}+{D}={A}+{C}+\left({B}+{D}\right)$
11 10 3expa ${⊢}\left(\left({A}\in ℂ\wedge {C}\in ℂ\right)\wedge {B}+{D}\in ℂ\right)\to {A}+{C}+{B}+{D}={A}+{C}+\left({B}+{D}\right)$
12 9 11 sylan2 ${⊢}\left(\left({A}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({B}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{C}+{B}+{D}={A}+{C}+\left({B}+{D}\right)$
13 12 an4s ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{C}+{B}+{D}={A}+{C}+\left({B}+{D}\right)$
14 4 8 13 3eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{B}+{C}+{D}={A}+{C}+{B}+{D}$