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

Metamath Proof Explorer

Theorem mvrrsubd

Description: Move a subtraction in the RHS to a right-addition in the LHS. Converse of mvlraddd .

EDITORIAL: Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024)

Ref Expression
Hypotheses mvrrsubd.a ⊢ φ → B ∈ ℂ
mvrrsubd.b ⊢ φ → C ∈ ℂ
mvrrsubd.1 ⊢ φ → A = B − C
Assertion mvrrsubd ⊢ φ → A + C = B

Proof

Step Hyp Ref Expression
1 mvrrsubd.a ⊢ φ → B ∈ ℂ
2 mvrrsubd.b ⊢ φ → C ∈ ℂ
3 mvrrsubd.1 ⊢ φ → A = B − C
4 1 2 subcld ⊢ φ → B − C ∈ ℂ
5 3 4 eqeltrd ⊢ φ → A ∈ ℂ
6 5 2 addcld ⊢ φ → A + C ∈ ℂ
7 5 2 pncand ⊢ φ → A + C - C = A
8 7 3 eqtrd ⊢ φ → A + C - C = B − C
9 6 1 2 8 subcan2d ⊢ φ → A + C = B