Theorem rmul_distr_add

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 1, 2 ⊢ a + b ∈ ℝ, radd_closed 1 2.
05. 1, 2, 3 ⊢ (a + b)⋅c = c⋅(a + b), rmul_comm 4 3.
06. 1, 2, 3 ⊢ c⋅(a + b) = c⋅a + c⋅b, rmul_distl_add 3 1 2.
07. 1, 3 ⊢ c⋅a = a⋅c, rmul_comm 3 1.
08. 2, 3 ⊢ c⋅b = b⋅c, rmul_comm 3 2.
09. 1, 2, 3 ⊢ c⋅(a + b) = a⋅c + c⋅b, eq_subst 7 6,
  P t ↔ c⋅(a + b) = t + c⋅b.
10. 1, 2, 3 ⊢ c⋅(a + b) = a⋅c + b⋅c, eq_subst 8 9,
  P t ↔ c⋅(a + b) = a⋅c + t.
11. 1, 2, 3 ⊢ (a + b)⋅c = a⋅c + b⋅c, eq_trans 5 10.
rmul_distr_add. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  (a + b)⋅c = a⋅c + b⋅c, subj_intro_iii 11.

Dependencies
The given proof depends on five axioms:
eq_refl, eq_subst, radd_closed, rmul_comm, rmul_distl_add.