diag_contra

Theorem diag_contra

Theorem. diag_contra
(A ↔ ¬A) → ⊥

Proof
01. 1 ⊢ A ↔ ¬A, hypo.
02. 1 ⊢ A → ¬A, bij_eliml 1.
03. 3 ⊢ A, hypo.
04. 1, 3 ⊢ ¬A, subj_elim 2 3.
05. 1, 3 ⊢ ⊥, neg_elim 4 3.
06. 1 ⊢ ¬A, neg_intro 5.
07. 1 ⊢ ¬A → A, bij_elimr 1.
08. 1 ⊢ A, subj_elim 7 6.
09. 1 ⊢ ⊥, neg_elim 6 8.
diag_contra. ⊢ (A ↔ ¬A) → ⊥, subj_intro 9.