equi_trans

Theorem equi_trans

Theorem. equi_trans
(A ↔ B) → (B ↔ C) → (A ↔ C)

Proof
01. 1 ⊢ A ↔ B, hypo.
02. 2 ⊢ B ↔ C, hypo.
03. 1 ⊢ A → B, bij_eliml 1.
04. 2 ⊢ B → C, bij_eliml 2.
05. 1 ⊢ B → A, bij_elimr 1.
06. 2 ⊢ C → B, bij_elimr 2.
07. 1, 2 ⊢ A → C, hypothetical_syllogism 3 4.
08. 1, 2 ⊢ C → A, hypothetical_syllogism 6 5.
09. 1, 2 ⊢ A ↔ C, bij_intro 7 8.
equi_trans. ⊢ (A ↔ B) → (B ↔ C) → (A ↔ C), subj_intro_ii 9.