This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
	Assertion	speimfwALT	⊢ ( ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		speimfw.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
2	1	eximi	⊢ ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ( 𝜑 → 𝜓 ) )
3		df-ex	⊢ ( ∃ 𝑥 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦 )
4		19.35	⊢ ( ∃ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )
5	2 3 4	3imtr3i	⊢ ( ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )