Пусть Φ Ψ — формулы исчисления предикатов

Придерживаемся следующей аксиоматики (Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. — 5-е изд., исправл., — М.: ФИЗМАТЛИТ, 2004. — 256 с., стр. 91):
Ψ(x)→∃yΨ(y) — аксиома 12,
∀xΨ(x)→Ψ(x) — аксиома 11,
∀xΨ(x)→∃yΨ(y) — из (1) и (2) по правилу modus ponens,
Φ(x,y)→∃zΦ(z,y) — аксиома 12 (с учётом оговоренных условий),
∃zΦ(z,y)→∃x∃zΦ(z,x) — аксиома 12 (с учётом оговоренных условий),
Φ(x,y)→∃x∃zΦ(z,x) — из (4) и(5) по правилу силлогизма,
∃x∃zΦ(z,x)→ ∃x∃zΦ(z,x)∨∃xΨ(x) — аксиома 6,
Φ(x,y)→∃x∃zΦ(z,x)∨∃xΨ(x) — из (6) и(7) по правилу силлогизма,
Ψ(x)→∃xΨ(x) — аксиома 12 (с учётом оговоренных условий),
∃xΨ(x)→∃x∃zΦ(z,x)∨∃xΨ(x) — аксиома 7,
Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x) — из (9) и(10) по правилу силлогизма,
Φ(x,y)→∃x∃zΦ(z,x)∨∃xΨ(x)→Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x)→Φ(x,y)∨Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x) — аксиома 8,
Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x)→Φ(x,y)∨Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x) — из (12) и (8) по правилу modus ponens,
Φ(x,y)∨Ψ(x)→∃x∃zΦ(z,x)∨∃xΨ(x) — из (13) и (11) по правилу modus ponens,
∃x∃zΦ(z,x)∨∃xΨ(x) — из (14) и (3) по правилу modus ponens.