# Metamath Proof Explorer

Description: Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005)

Ref Expression
Assertion addsub4 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{B}-\left({C}+{D}\right)=\left({A}-{C}\right)+{B}-{D}$

### Proof

Step Hyp Ref Expression
1 simpll ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}\in ℂ$
2 simplr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {B}\in ℂ$
3 simprl ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {C}\in ℂ$
4 addsub ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}+{B}-{C}={A}-{C}+{B}$
5 1 2 3 4 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{B}-{C}={A}-{C}+{B}$
6 5 oveq1d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to \left({A}+{B}\right)-{C}-{D}=\left({A}-{C}\right)+{B}-{D}$
7 1 2 addcld ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{B}\in ℂ$
8 simprr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {D}\in ℂ$
9 subsub4 ${⊢}\left({A}+{B}\in ℂ\wedge {C}\in ℂ\wedge {D}\in ℂ\right)\to \left({A}+{B}\right)-{C}-{D}={A}+{B}-\left({C}+{D}\right)$
10 7 3 8 9 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to \left({A}+{B}\right)-{C}-{D}={A}+{B}-\left({C}+{D}\right)$
11 subcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\right)\to {A}-{C}\in ℂ$
12 11 ad2ant2r ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}-{C}\in ℂ$
13 addsubass ${⊢}\left({A}-{C}\in ℂ\wedge {B}\in ℂ\wedge {D}\in ℂ\right)\to \left({A}-{C}\right)+{B}-{D}=\left({A}-{C}\right)+{B}-{D}$
14 12 2 8 13 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to \left({A}-{C}\right)+{B}-{D}=\left({A}-{C}\right)+{B}-{D}$
15 6 10 14 3eqtr3d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\in ℂ\wedge {D}\in ℂ\right)\right)\to {A}+{B}-\left({C}+{D}\right)=\left({A}-{C}\right)+{B}-{D}$