Theorem eq_symm_trans

Proof
01. 1 ⊢ y = x, hypo.
02. 2 ⊢ y = z, hypo.
03. 1 ⊢ x = y, eq_symm 1.
04. 1, 2 ⊢ x = z, eq_trans 3 2.
eq_symm_trans. ⊢ y = x → y = z → x = z, subj_intro_ii 4.

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