Theorem spimv

A version of spim with a distinct variable requirement instead of a bound-variable hypothesis. See spimfv and spimvw for versions requiring fewer axioms. (Contributed by NM, 31-Jul-1993.) Usage of this theorem is discouraged because it depends on [ax-13]. Use spimvw instead. (New usage is discouraged.)

Hypothesis
spimv.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \psi \)
Proof
l0
nfv
\( \vdash \Finv x \, \psi \)
spimv.1
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
spim l0 _