Theorem spnfw

Weak version of sp. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 13-Aug-2017.)

Hypothesis
spnfw.1
\( \vdash \neg \varphi \rightarrow \forall x \, \neg \varphi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \varphi \)
Proof
l0
spnfw.1
\( \vdash \neg \varphi \rightarrow \forall x \, \neg \varphi \)
idd
\( \vdash x = y \rightarrow \varphi \rightarrow \varphi \)
spimw l0 _