Theorem eq_subst_rev

Theorem. eq_subst_rev
y = x → P x → P y
Proof
01. 1 ⊢ y = x, hypo.
02. 1 ⊢ x = y, eq_symm 1.
03. 1 ⊢ P x → P y, subj_elim eq_subst 2.
eq_subst_rev. ⊢ y = x → P x → P y, subj_intro 3.

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