radd_perm

Theorem radd_perm_231

Theorem. radd_perm_231
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + b + c = b + c + a

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 1, 2 ⊢ a + b + c = b + a + c, radd_perm_213 1 2.
05. 1, 2, 3 ⊢ b + a + c = b + c + a, radd_perm_132 2 1 3.
06. 1, 2, 3 ⊢ a + b + c = b + c + a, eq_trans 4 5.
radd_perm_231. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a + b + c = b + c + a, subj_intro_iii 6.

Dependencies
The given proof depends on four axioms:
eq_refl, eq_subst, radd_assoc, radd_comm.