radd_assoc_llloolo

Theorem radd_assoc_llloolo

Theorem. radd_assoc_llloolo
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a + b + c + d = a + (b + c) + d

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 1, 2, 3 ⊢ a + b + c = a + (b + c), radd_assoc 1 2 3.
05. 1, 2, 3 ⊢ a + b + c + d = a + (b + c) + d,
  eq_cong 4, f t = t + d.
radd_assoc_llloolo. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a + b + c + d = a + (b + c) + d, subj_intro_iii 5.

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