radd_perm

Theorem radd_perm_213

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

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 1, 2 ⊢ a + b = b + a, radd_comm 1 2.
04. 1, 2 ⊢ a + b + c = b + a + c, eq_cong 3, f t = t + c.
radd_perm_213. ⊢ a ∈ ℝ → b ∈ ℝ → a + b + c = b + a + c,
  subj_intro_ii 4.

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