Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ b ∈ ℝ, hypo. 03. 3 ⊢ c ∈ ℝ, hypo. 04. 1, 2, 3 ⊢ a + b + c = a + c + b, radd_perm_132 1 2 3. 05. 1, 3 ⊢ a + c + b = c + a + b, radd_perm_213 1 3. 06. 1, 2, 3 ⊢ a + b + c = c + a + b, eq_trans 4 5. radd_perm_312. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + b + c = c + a + b, subj_intro_iii 6.
Dependencies
The given proof depends on four axioms:
eq_refl, eq_subst, radd_assoc, radd_comm.