Theorem eq_trans_rr

Transitive law of equality with right hand sides bridging. This variant of eq_trans allows the omission of eq_symm, which improves ergonomics.

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

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