Theorem spimw

Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.)

Hypotheses
spimw.1
\( \vdash \neg \psi \rightarrow \forall x \, \neg \psi \)
spimw.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \psi \)
Proof
l0
ax6v
\( \vdash \neg \forall x \, \neg x = y' \)
l1
spimw.1
spimw.2
spimfw l1 _
\( \vdash \neg \forall x \, \neg x = y' \rightarrow \forall x \, \varphi \rightarrow \psi \)
ax-mp l0 _