Theorem spfw

Weak version of sp. Uses only Tarski's FOL axiom schemes. Lemma 9 of [KalishMontague] p. 87. This may be the best we can do with minimal distinct variable conditions. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.)

Hypotheses
spfw.1
\( \vdash \neg \psi \rightarrow \forall x \, \neg \psi \)
spfw.2
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \forall x \, \varphi \)
spfw.3
\( \vdash \neg \varphi \rightarrow \forall y \, \neg \varphi \)
spfw.4
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \varphi \)
Proof
l0
spfw.2
l1
spfw.1
spfw.4
biimpd _
l4
cbvaliw l0 l1 _
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \psi \)
l5
spfw.3
\( \vdash \neg \varphi \rightarrow \forall y \, \neg \varphi \)
spfw.4
biimprd _
equcoms _
\( \vdash y = x \rightarrow \psi \rightarrow \varphi \)
spimw l5 _
\( \vdash \forall y \, \psi \rightarrow \varphi \)
syl l4 _