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

Metamath Proof Explorer

Theorem repncan3

Description: Addition and subtraction of equals. Based on pncan3 . (Contributed by Steven Nguyen, 8-Jan-2023)

Ref Expression
Assertion repncan3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B - ℝ A = B

Proof

Step Hyp Ref Expression
1 rersubcl ⊢ B ∈ ℝ ∧ A ∈ ℝ → B - ℝ A ∈ ℝ
2 eqid ⊢ B - ℝ A = B - ℝ A
3 resubadd ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ B - ℝ A ∈ ℝ → B - ℝ A = B - ℝ A ↔ A + B - ℝ A = B
4 2 3 mpbii ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ B - ℝ A ∈ ℝ → A + B - ℝ A = B
5 1 4 mpd3an3 ⊢ B ∈ ℝ ∧ A ∈ ℝ → A + B - ℝ A = B
6 5 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B - ℝ A = B