Theorem spfalw

Version of sp when \( \varphi \) is false. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 25-Dec-2017.)

Hypothesis
spfalw.1
\( \vdash \neg \varphi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \varphi \)
Proof
spfalw.1
hbth _
spnfw _