Theorem equi_cong_subj

Proof
01. 1 ⊢ A ↔ A', hypo.
02. 2 ⊢ B ↔ B', hypo.
03. 3 ⊢ A → B, hypo.
04. 4 ⊢ A', hypo.
05. 1, 4 ⊢ A, rsubj_elim 1 4.
06. 1, 3, 4 ⊢ B, subj_elim 3 5.
07. 1, 2, 3, 4 ⊢ B', lsubj_elim 2 6.
08. 1, 2 ⊢ (A → B) → (A' → B'), subj_intro_ii 7.
09. 9 ⊢ A' → B', hypo.
10. 10 ⊢ A, hypo.
11. 1, 10 ⊢ A', lsubj_elim 1 10.
12. 1, 9, 10 ⊢ B', subj_elim 9 11.
13. 1, 2, 9, 10 ⊢ B, rsubj_elim 2 12.
14. 1, 2 ⊢ (A' → B') → (A → B), subj_intro_ii 13.
15. 1, 2 ⊢ (A → B) ↔ (A' → B'), bij_intro 8 14.
equi_cong_subj. ⊢ (A ↔ A') → (B ↔ B') →
  ((A → B) ↔ (A' → B')), subj_intro_ii 15.