Theorem iadd_assoc

Proof
iadd_assoc. ⊢ a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → (a + b) + c = a + (b + c),
  pred_iii_restr int_incl_in_real radd_assoc.

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