матлогика, гильбертовское исчисление

[nisir]

($\Phi$ -> $\Psi$) -> ($\forall x\Phi$ -> $\Psi$)

не могу избавиться от квантора, дальше вывод хотя-бы более менее понятен..

[Профессор Снэйп]

Как всегда, теорема о дедукции.