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

Metamath Proof Explorer

Theorem subeqxfrd

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

Ref Expression
Hypotheses subeqxfrd.a ⊢ φ → A ∈ ℂ
subeqxfrd.b ⊢ φ → B ∈ ℂ
subeqxfrd.c ⊢ φ → C ∈ ℂ
subeqxfrd.d ⊢ φ → D ∈ ℂ
subeqxfrd.1 ⊢ φ → A − B = C − D
Assertion subeqxfrd ⊢ φ → A − C = B − D

Proof

Step Hyp Ref Expression
1 subeqxfrd.a ⊢ φ → A ∈ ℂ
2 subeqxfrd.b ⊢ φ → B ∈ ℂ
3 subeqxfrd.c ⊢ φ → C ∈ ℂ
4 subeqxfrd.d ⊢ φ → D ∈ ℂ
5 subeqxfrd.1 ⊢ φ → A − B = C − D
6 5 oveq1d ⊢ φ → A − B + B - C = C − D + B - C
7 1 2 3 npncand ⊢ φ → A − B + B - C = A − C
8 3 4 2 npncan3d ⊢ φ → C − D + B - C = B − D
9 6 7 8 3eqtr3d ⊢ φ → A − C = B − D