Theorem equi_cong_conj

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