Theorem equi_cong_neg

Proof
01. 1 ⊢ A ↔ A', hypo.
02. 2 ⊢ ¬A, hypo.
03. 3 ⊢ A', hypo.
04. 1, 3 ⊢ A, rsubj_elim 1 3.
05. 1, 2, 3 ⊢ ⊥, neg_elim 2 4.
06. 1, 2 ⊢ ¬A', neg_intro 5.
07. 1 ⊢ ¬A → ¬A', subj_intro 6.
08. 8 ⊢ ¬A', hypo.
09. 9 ⊢ A, hypo.
10. 1, 9 ⊢ A', lsubj_elim 1 9.
11. 1, 8, 9 ⊢ ⊥, neg_elim 8 10.
12. 1, 8 ⊢ ¬A, neg_intro 11.
13. 1 ⊢ ¬A' → ¬A, subj_intro 12.
14. 1 ⊢ ¬A ↔ ¬A', bij_intro 7 13.
equi_cong_neg. ⊢ (A ↔ A') → (¬A ↔ ¬A'),
  subj_intro 14.