Metamath Proof Explorer

Theorem subadd4

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

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

Proof

Step Hyp Ref Expression
1 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
2 subsub2 ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) − ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) + ( 𝐷 − 𝐶 ) ) )
3 2 3expb ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 − 𝐵 ) − ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) + ( 𝐷 − 𝐶 ) ) )
4 1 3 sylan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 − 𝐵 ) − ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) + ( 𝐷 − 𝐶 ) ) )
5 addsub4 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) → ( ( 𝐴 + 𝐷 ) − ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 − 𝐵 ) + ( 𝐷 − 𝐶 ) ) )
6 5 an42s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐷 ) − ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 − 𝐵 ) + ( 𝐷 − 𝐶 ) ) )
7 4 6 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 − 𝐵 ) − ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 + 𝐷 ) − ( 𝐵 + 𝐶 ) ) )