Theorem spsv

Generalization of antecedent. A trivial weak version of sps avoiding [ax-12]. (Contributed by SN, 13-Nov-2025.) (Proof shortened by WL, 19-Nov-2025.)

Hypothesis
spsv.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \psi \)
Proof
spsv.1
a1i _
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
spimvw _