Theorem intersection_assocr

Proof
intersection_assocr. ⊢ A ∩ (B ∩ C) = (A ∩ B) ∩ C,
  eq_symm intersection_assocl.

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