Формальная логика - Вывод правила исключения коньюнкции

[quuxity]

Помогите пожалуйста в стандартном исчислении высказываний L (3 аксиомы и modus ponens) вывести правило исключения коньюнкции:

$\neg (A \to \neg B) \vdash A$

UPD:
<тут был чей-то пост с предложением упростить выражение слева. ниже ответ на него>
В каком смысле упростить? Применить к нему сколько-нибудь раз одну из стандартных аксиом и/или общепринятых теорем L (из книги в книгу обычно 6-7 одних и тех же теорем) так, чтобы оно стало короче?
Из широкоизвестных теорем, которые применяются непосредственно, есть вот такая:
Тneg: $\neg A \to (A \to B)$
1. $\neg (A \to \neg B)$ -- гипотеза
2. $\neg (A \to \neg B) \to ((A \to \neg B) \to X)$ -- Tneg [$A \to \neg B$ / A, X / B]
3. $(A \to \neg B) \to X$ -- Modus-Ponens (1, 2)
Потом можно применить одно из следствий теоремы дедукции:
4. $ \neg B \to X$ -- правило устранения крайнего
Вот и упростил вроде.

[Nemiroff]

Если у вас есть $\neg A \to (A \to \neg B)$ вдобавок к $(\neg B \to \neg A)\to(A \to B)$, то вроде все понятно.

[Maslov]

Решение этого примера есть в задачнике Игошина.

[quuxity]

Nemiroff, Maslov
Спасибо, действительно очень просто.

$\newline 0. \vdash \neg (A \to \neg B) \to A \newline 1. \neg (A \to \neg B) \vdash A, [$теорема дедукции (0)]$ \newline 2. \neg (A \to \neg B), [$гипотеза$] \newline 3. \neg (A \to \neg B) \to ((A \to \neg B) \to \neg \neg (A \to \neg B)), [$Ti$] \newline 4. (A \to \neg B) \to \neg \neg (A \to \neg B), [$modus ponens (2,3)$] \newline 5. \neg B \to \neg \neg (A \to \neg B), [$правило удаления крайнего (4)$] \newline 6. \neg (A \to \neg B) \to B, [$Tj (5)$] \newline 7. B, [$modus ponens (2,6)$] \newline 8. B \to (\neg A \to \neg (\neg A \to B)), [$Tk$] \newline 9. \neg A \to \neg (\neg A \to B), [$modus ponens (7,8)$] \newline 10. (\neg A \to \neg (\neg A \to B)) \to ((\neg A \to B) \to A), [$Tj (9)$] \newline 11. (\neg A \to B) \to A, [$modus ponens(9,10)$] \newline 12. B \to A, [$правило удаления крайнего (11)$] \newline 13. A, [$modus ponens (7,12)$] $

, где Ti, Tj, Tk - относительно общепринятые теоремы исчисления высказываний L.