Theorem spimehOLD

Description: Obsolete version of spimew as of 22-Oct-2023. (Contributed by NM, 7-Aug-1994) (Proof shortened by Wolf Lammen, 10-Dec-2017) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	spimew.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	spimew.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
Assertion	spimehOLD	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		spimew.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		spimew.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
3		ax6ev	⊢ ∃ 𝑥 𝑥 = 𝑦
4	3 2	eximii	⊢ ∃ 𝑥 ( 𝜑 → 𝜓 )
5	4	19.35i	⊢ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 )
6	1 5	syl	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )