Theorem equi_trans_ll

Transitive law of logical equivalence with left hand sides bridging. This variant of equi_trans allows the omission of equi_symm, which improves ergonomics.

Proof
01. 1 ⊢ C ↔ A, hypo.
02. 2 ⊢ C ↔ B, hypo.
03. 1 ⊢ A ↔ C, equi_symm 1.
04. 1, 2 ⊢ A ↔ B, equi_trans 3 2.
equi_trans_ll. ⊢ (C ↔ A) → (C ↔ B) → (A ↔ B),
  subj_intro_ii 4.