Theorem nadd_assoc

Proof
nadd_assoc. ⊢ a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → (a + b) + c = a + (b + c),
  pred_iii_restr nat_incl_in_real radd_assoc.

Dependencies
The given proof depends on five axioms:
comp, eq_subst, radd_assoc, radd_closed, real_is_set.