Theorem equi_cong_bij

Proof
01. 1 ⊢ A ↔ A', hypo.
02. 2 ⊢ B ↔ B', hypo.
03. 3 ⊢ A ↔ B, hypo.
04. 1, 3 ⊢ A' ↔ B, equi_trans_ll 1 3.
05. 1, 2, 3 ⊢ A' ↔ B', equi_trans 4 2.
06. 1, 2 ⊢ (A ↔ B) → (A' ↔ B'), subj_intro 5.
07. 7 ⊢ A' ↔ B', hypo.
08. 1, 7 ⊢ A ↔ B', equi_trans 1 7.
09. 1, 2, 7 ⊢ A ↔ B, equi_trans_rr 8 2.
10. 1, 2 ⊢ (A' ↔ B') → (A ↔ B), subj_intro 9.
11. 1, 2 ⊢ (A ↔ B) ↔ (A' ↔ B'), bij_intro 6 10.
equi_cong_bij. ⊢ (A ↔ A') → (B ↔ B') →
  ((A ↔ B) ↔ (A' ↔ B')), subj_intro_ii 11.