¬ ∀𝑥((∃𝑦 𝑃(𝑥, 𝑦) ∧ ∃𝑦 𝑄(𝑥, 𝑦)) → ∃𝑦(𝑃(𝑥, 𝑦) ∨ 𝑄(𝑥, 𝑦)
¬ ∀𝑥(¬(∃𝑦 𝑃(𝑥, 𝑦) ∧ ∃𝑦 𝑄(𝑥, 𝑦)) \/ ∃𝑦(𝑃(𝑥, 𝑦) ∨ 𝑄(𝑥, 𝑦))
 ∃𝑥(¬¬(∃𝑦 𝑃(𝑥, 𝑦) ∧ ∃𝑦 𝑄(𝑥, 𝑦)) /\ ¬∃𝑦(𝑃(𝑥, 𝑦) ∨ 𝑄(𝑥, 𝑦))
∃𝑥((∃𝑦 𝑃(𝑥, 𝑦) ∧ ∃𝑦 𝑄(𝑥, 𝑦)) /\ ∀𝑦¬(𝑃(𝑥, 𝑦) ∨ 𝑄(𝑥, 𝑦))
∃𝑥((∃𝑦 𝑃(𝑥, 𝑦) ∧ ∃𝑦 𝑄(𝑥, 𝑦)) /\ ∀𝑦(¬𝑃(𝑥, 𝑦) ∧ ¬𝑄(𝑥, 𝑦))
∃𝑥((∃𝑦 𝑃(𝑥, 𝑦) ∧ ∃z 𝑄(𝑥, z)) /\ ∀w(¬𝑃(𝑥, w) ∧ ¬𝑄(𝑥, w))
((∃𝑦 𝑃(X, 𝑦) ∧ ∃z 𝑄(X, z)) /\ ∀w(¬𝑃(X, w) ∧ ¬𝑄(X, w))
((𝑃(X, Y) ∧ 𝑄(X, Z)) /\ ∀w(¬𝑃(X, w) ∧ ¬𝑄(X, w))
∀w ((𝑃(X, Y) ∧ 𝑄(X, Z)) /\ (¬𝑃(X, w) ∧ ¬𝑄(X, w))

𝑃(X, Y)
𝑄(X, Z)
¬𝑃(X, w)
¬𝑄(X, w)

============================================

∀𝑥(𝑃(𝑥) → ∃𝑦 ∀𝑧 𝑄(𝑓(𝑥, 𝑦), 𝑧))
∀𝑥(¬𝑃(𝑥) \/ ∃𝑦 ∀𝑧 𝑄(𝑓(𝑥, 𝑦), 𝑧))
fy(x)
∀𝑥(¬𝑃(𝑥) \/ ∀𝑧 𝑄(𝑓(𝑥, fy(x)), 𝑧))
∀𝑥∀𝑧(¬𝑃(𝑥) \/ 𝑄(𝑓(𝑥, fy(x)), 𝑧))


¬𝑃(𝑥) \/ 𝑄(𝑓(𝑥, fy(x)), 𝑧)

============================================
∀𝑥(∃𝑦 ∀𝑧 𝑄(𝑓(𝑥, 𝑦), 𝑧) → 𝑃(𝑥))
∀𝑥(¬∃𝑦 ∀𝑧 𝑄(𝑓(𝑥, 𝑦), 𝑧) \/ 𝑃(𝑥))
∀𝑥(∀𝑦 ¬ ∀𝑧 𝑄(𝑓(𝑥, 𝑦), 𝑧) \/ 𝑃(𝑥))
∀𝑥(∀𝑦 ∃𝑧 ¬𝑄(𝑓(𝑥, 𝑦), 𝑧) \/ 𝑃(𝑥))
fz(x,y)
∀𝑥(∀𝑦 ¬𝑄(𝑓(𝑥, 𝑦), fz(x,y)) \/ 𝑃(𝑥))
∀𝑥 ∀𝑦 (¬𝑄(𝑓(𝑥, 𝑦), fz(x,y)) \/ 𝑃(𝑥))

¬𝑄(𝑓(𝑥, 𝑦), fz(x,y)) \/ 𝑃(𝑥)

