Theorem speimfwALT

Alternate proof of speimfw (longer compressed proof, but fewer essential steps). (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Aug-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
speimfw.2
\( \vdash x = y' \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \neg \forall x \, \neg x = y' \rightarrow \forall x \, \varphi \rightarrow \exists x \, \psi \)
Proof
speimfw.2
l1
eximi _
\( \vdash \exists x \, x = y' \rightarrow \exists x \, (\varphi \rightarrow \psi) \)
l2
df-ex
\( \vdash \exists x \, x = y' \leftrightarrow \neg \forall x \, \neg x = y' \)
19.35
\( \vdash \exists x \, (\varphi \rightarrow \psi) \leftrightarrow \forall x \, \varphi \rightarrow \exists x \, \psi \)
3imtr3i l1 l2 _