Theorem radd_assoc_llloloo

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

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