Theorem spim

Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim series of theorems requires that only one direction of the substitution hypothesis hold. Usage of this theorem is discouraged because it depends on [ax-13]. See spimw for a version requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) (New usage is discouraged.)

Hypotheses
spim.1
\( \vdash \Finv x \, \psi \)
spim.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \psi \)
Proof
l0
spim.1
l1
ax6e
\( \vdash \exists x \, x = y' \)
spim.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
eximii l1 _
19.36i l0 _