Theorem radd_cancel

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 1, 2 ⊢ a + b ∈ ℝ, radd_closed 1 2.
04. 2 ⊢ -b ∈ ℝ, rneg_closed 2.
05. ⊢ a + b - b = a + b + -b, rsub_eq.
06. 1, 2 ⊢ a + b + -b = a + (b + -b), radd_assoc 1 2 4.
07. 1, 2 ⊢ a + b - b = a + (b + -b), eq_trans 5 6.
08. 2 ⊢ b + -b = 0, radd_inv 2.
09. 1, 2 ⊢ a + b - b = a + 0, eq_subst 8 7,
  P t ↔ a + b - b = a + t.
10. 1 ⊢ a + 0 = a, radd_neutr 1.
11. 1, 2 ⊢ a + b - b = a, eq_trans 9 10.
radd_cancel. ⊢ a ∈ ℝ → b ∈ ℝ → a + b - b = a,
  subj_intro_ii 11.

Dependencies
The given proof depends on seven axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_inv, radd_neutr, rneg_closed.