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 ⊢ φ → A ∈ ℂ
subaddeqd.b ⊢ φ → B ∈ ℂ
subaddeqd.c ⊢ φ → C ∈ ℂ
subaddeqd.d ⊢ φ → D ∈ ℂ
subaddeqd.1 ⊢ φ → A + B = C + D
Assertion subaddeqd ⊢ φ → A − D = C − B

Proof

Step Hyp Ref Expression
1 subaddeqd.a ⊢ φ → A ∈ ℂ
2 subaddeqd.b ⊢ φ → B ∈ ℂ
3 subaddeqd.c ⊢ φ → C ∈ ℂ
4 subaddeqd.d ⊢ φ → D ∈ ℂ
5 subaddeqd.1 ⊢ φ → A + B = C + D
6 5 oveq1d ⊢ φ → A + B - D + B = C + D - D + B
7 3 4 addcomd ⊢ φ → C + D = D + C
8 7 oveq1d ⊢ φ → C + D - D + B = D + C - D + B
9 6 8 eqtrd ⊢ φ → A + B - D + B = D + C - D + B
10 1 4 2 pnpcan2d ⊢ φ → A + B - D + B = A − D
11 4 3 2 pnpcand ⊢ φ → D + C - D + B = C − B
12 9 10 11 3eqtr3d ⊢ φ → A − D = C − B