Построить вывод в ИВ

[Patich]

Необходимо построить формальный вывод в ИВ, используя аксиомы Клини и "Modus ponens"
$\vdash (¬A \vee ¬B) \to ¬(A \wedge B)$

Довел лишь до необходимости доказательства
¬A \to ((A \wedge B)\to ¬B)

[Maslov]

А теоремой о дедукции и правилами введения/удаления связок можно пользоваться?

[Patich]

Теоремой о дедукции пользоваться можно. А правилами нельзя.