Theorem speimfwALT

Description: 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.)

	Ref	Expression
Hypothesis	speimfw.2	$$⊢x=y\to \left(\phi \to \psi \right)$$
Assertion	speimfwALT	$$⊢\neg \forall x\neg x=y\to \left(\forall x\phi \to \exists x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		speimfw.2	$$⊢x=y\to \left(\phi \to \psi \right)$$
2	1	eximi	$$⊢\exists xx=y\to \exists x\left(\phi \to \psi \right)$$
3		df-ex	$$⊢\exists xx=y\leftrightarrow \neg \forall x\neg x=y$$
4		19.35	$$⊢\exists x\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\phi \to \exists x\psi \right)$$
5	2 3 4	3imtr3i	$$⊢\neg \forall x\neg x=y\to \left(\forall x\phi \to \exists x\psi \right)$$