Theorem spv

Specialization, using implicit substitution. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker spvv if possible. (Contributed by NM, 30-Aug-1993.) (New usage is discouraged.)

Hypothesis

spv.1

\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)

Conclusion

\( \vdash \forall x \, \varphi \rightarrow \psi \)

Proof

spv.1

biimpd _

\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)

spimv _