Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ b ∈ ℝ, hypo. 03. 3 ⊢ c ∈ ℝ, hypo. 04. 4 ⊢ c + a = b + c, hypo. 05. 1, 3 ⊢ a + c = c + a, radd_comm 1 3. 06. 1, 3, 4 ⊢ a + c = b + c, eq_trans 5 4. 07. 1, 2, 3, 4 ⊢ a = b, radd_cancel_rr 1 2 3 6. radd_cancel_lr. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → c + a = b + c → 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.