Theorem equi_trans_rr

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

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