Theorem rsub_cancel_middle

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. ⊢ a - b = a + -b, rsub_eq.
05. ⊢ b - c = b + -c, rsub_eq.
06. ⊢ (a - b) + (b - c) = (a + -b) + (b + -c),
  eq_cong_ii 4 5, f x y = x + y.
07. 2 ⊢ -b ∈ ℝ, rneg_closed 2.
08. 3 ⊢ -c ∈ ℝ, rneg_closed 3.
09. 1, 2, 3 ⊢ a + -b + b + -c = (a + -b) + (b + -c),
  radd_assoc_llolloo 1 7 2 8.
10. 1, 2 ⊢ a + -b + b + -c = a + (-b + b) + -c,
  radd_assoc_llloolo 1 7 2.
11. 1, 2, 3 ⊢ (a + -b) + (b + -c) = a + (-b + b) + -c,
  eq_trans_ll 9 10.
12. 1, 2, 3 ⊢ (a - b) + (b - c) = a + (-b + b) + -c,
  eq_trans 6 11.
13. 2 ⊢ -b + b = b + -b, radd_comm 7 2.
14. 2 ⊢ b + -b = 0, radd_inv 2.
15. 2 ⊢ -b + b = 0, eq_trans 13 14.
16. 2 ⊢ a + (-b + b) = a + 0, eq_cong 15, f x = a + x.
17. 1 ⊢ a + 0 = a, radd_neutr 1.
18. 1, 2 ⊢ a + (-b + b) = a, eq_trans 16 17.
19. 1, 2, 3 ⊢ (a - b) + (b - c) = a + -c,
  eq_subst 18 12, P t ↔ (a - b) + (b - c) = t + -c.
20. ⊢ a - c = a + -c, rsub_eq.
21. 1, 2, 3 ⊢ (a - b) + (b - c) = a - c, eq_trans_rr 19 20.
rsub_cancel_middle. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  (a - b) + (b - c) = a - c, subj_intro_iii 21.

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