Theorem eq_trans_ll

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

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_trans_ll. ⊢ y = x → y = z → x = z, subj_intro_ii 4.

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