radd_assoc_llllooo

Theorem radd_assoc_llllooo

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

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 = b + (c + d), radd_assoc 2 3 4.
07. 1, 2, 3, 4 ⊢ a + b + c + d = a + (b + (c + d)),
  eq_subst 6 5, P t ↔ a + b + c + d = a + t.
radd_assoc_llllooo. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → d ∈ ℝ →
  a + b + c + d = a + (b + (c + d)), subj_intro_iv 7.

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