Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ b ∈ ℝ, hypo. 03. 3 ⊢ c ∈ ℝ, hypo. 04. 4 ⊢ a + c = c + b, hypo. 05. 2, 3 ⊢ c + b = b + c, radd_comm 3 2. 06. 2, 3, 4 ⊢ a + c = b + c, eq_trans 4 5. 07. 1, 2, 3, 4 ⊢ a = b, radd_cancel_rr 1 2 3 6. radd_cancel_rl. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + c = c + b → a = b, subj_intro_iv 7.
Dependencies
The given proof depends on eight axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rneg_closed.