Theorem radd_perm_1423

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 4 ⊢ d ∈ ℝ, hypo.
05. 1, 2, 3, 4 ⊢ a + b + c + d = a + (b + c + d),
  radd_assoc_llloloo 1 2 3 4.
06. 2, 3, 4 ⊢ b + c + d = d + b + c,
  radd_perm_312 2 3 4.
07. 1, 2, 3, 4 ⊢ a + b + c + d = a + (d + b + c),
  eq_subst 6 5, P t ↔ a + b + c + d = a + t.
08. 1, 2, 3, 4 ⊢ a + d + b + c = a + (d + b + c),
  radd_assoc_llloloo 1 4 2 3.
09. 1, 2, 3, 4 ⊢ a + b + c + d = a + d + b + c,
  eq_trans_rr 7 8.
radd_perm_1423. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → d ∈ ℝ →
  a + b + c + d = a + d + b + c, subj_intro_iv 9.

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