radd_assoc_llolloo

Theorem radd_assoc_llolloo

Theorem. radd_assoc_llolloo
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. 3, 4 ⊢ c + d ∈ ℝ, radd_closed 3 4.
06. 1, 2, 3, 4 ⊢ a + b + (c + d) = a + (b + (c + d)),
  radd_assoc 1 2 5.
07. 1, 2, 3, 4 ⊢ a + b + c + d = a + (b + (c + d)),
  radd_assoc_llllooo 1 2 3 4.
08. 1, 2, 3, 4 ⊢ a + b + c + d = a + b + (c + d),
  eq_trans_rr 7 6.
radd_assoc_llolloo. ⊢ 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.