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