Theorem spimvw

A weak form of specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. For stronger forms using more axioms, see spimv and spimfv. (Contributed by NM, 9-Apr-2017.)

Hypothesis
spimvw.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \psi \)
Proof
l0
ax-5
\( \vdash \neg \psi \rightarrow \forall x \, \neg \psi \)
spimvw.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
spimw l0 _