This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subaddeqd

Description: Transfer two terms of a subtraction to an addition in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020)

Ref Expression
Hypotheses subaddeqd.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
subaddeqd.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
subaddeqd.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
subaddeqd.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
subaddeqd.1 ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
Assertion subaddeqd ( 𝜑 → ( 𝐴 − 𝐷 ) = ( 𝐶 − 𝐵 ) )

Proof

Step Hyp Ref Expression
1 subaddeqd.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 subaddeqd.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 subaddeqd.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4 subaddeqd.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5 subaddeqd.1 ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
6 5 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − ( 𝐷 + 𝐵 ) ) = ( ( 𝐶 + 𝐷 ) − ( 𝐷 + 𝐵 ) ) )
7 3 4 addcomd ⊢ ( 𝜑 → ( 𝐶 + 𝐷 ) = ( 𝐷 + 𝐶 ) )
8 7 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 + 𝐷 ) − ( 𝐷 + 𝐵 ) ) = ( ( 𝐷 + 𝐶 ) − ( 𝐷 + 𝐵 ) ) )
9 6 8 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − ( 𝐷 + 𝐵 ) ) = ( ( 𝐷 + 𝐶 ) − ( 𝐷 + 𝐵 ) ) )
10 1 4 2 pnpcan2d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − ( 𝐷 + 𝐵 ) ) = ( 𝐴 − 𝐷 ) )
11 4 3 2 pnpcand ⊢ ( 𝜑 → ( ( 𝐷 + 𝐶 ) − ( 𝐷 + 𝐵 ) ) = ( 𝐶 − 𝐵 ) )
12 9 10 11 3eqtr3d ⊢ ( 𝜑 → ( 𝐴 − 𝐷 ) = ( 𝐶 − 𝐵 ) )