Theorem intersection_elimr

Proof
01. 1 ⊢ x ∈ A ∩ B, hypo.
02. 1 ⊢ x ∈ A ∧ x ∈ B, intersection_elim 1.
03. 1 ⊢ x ∈ B, conj_elimr 2.
intersection_elimr. ⊢ x ∈ A ∩ B → x ∈ B, subj_intro 3.

Dependencies
The given proof depends on two axioms:
comp, eq_subst.