Theorem radd_perm_132

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 2, 3 ⊢ b + c = c + b, radd_comm 2 3.
05. 2, 3 ⊢ a + (b + c) = a + (c + b), eq_cong 4, f t = a + t.
06. 1, 2, 3 ⊢ a + b + c = a + (b + c), radd_assoc 1 2 3.
07. 1, 2, 3 ⊢ a + c + b = a + (c + b), radd_assoc 1 3 2.
08. 1, 2, 3 ⊢ a + b + c = a + (c + b), eq_trans 6 5.
09. 1, 2, 3 ⊢ a + b + c = a + c + b, eq_trans_rr 8 7.
radd_perm_132. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a + b + c = a + c + b, subj_intro_iii 9.

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