Theorem equi_cong_disj

Proof
01. 1 ⊢ A ↔ A', hypo.
02. 2 ⊢ B ↔ B', hypo.
03. 3 ⊢ A ∨ B, hypo.
04. 4 ⊢ A, hypo.
05. 1, 4 ⊢ A', lsubj_elim 1 4.
06. 1, 4 ⊢ A' ∨ B', disj_introl 5.
07. 7 ⊢ B, hypo.
08. 2, 7 ⊢ B', lsubj_elim 2 7.
09. 2, 7 ⊢ A' ∨ B', disj_intror 8.
10. 1, 2, 3 ⊢ A' ∨ B', disj_elim 3 6 9.
11. 1, 2 ⊢ A ∨ B → A' ∨ B', subj_intro 10.
12. 12 ⊢ A' ∨ B', hypo.
13. 13 ⊢ A', hypo.
14. 1, 13 ⊢ A, rsubj_elim 1 13.
15. 1, 13 ⊢ A ∨ B, disj_introl 14.
16. 16 ⊢ B', hypo.
17. 2, 16 ⊢ B, rsubj_elim 2 16.
18. 2, 16 ⊢ A ∨ B, disj_intror 17.
19. 1, 2, 12 ⊢ A ∨ B, disj_elim 12 15 18.
20. 1, 2 ⊢ A' ∨ B' → A ∨ B, subj_intro 19.
21. 1, 2 ⊢ A ∨ B ↔ A' ∨ B', bij_intro 11 20.
equi_cong_disj. ⊢ (A ↔ A') → (B ↔ B') →
  (A ∨ B ↔ A' ∨ B'), subj_intro_ii 21.