radd_perm

Theorem radd_perm_321

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

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

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