Theorem spimed

Description: Deduction version of spime . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker spimedv if possible. (Contributed by NM, 14-May-1993) (Revised by Mario Carneiro, 3-Oct-2016) (Proof shortened by Wolf Lammen, 19-Feb-2018) (New usage is discouraged.)

	Ref	Expression
Hypotheses	spimed.1	|- ( ch -> F/ x ph )
	spimed.2	|- ( x = y -> ( ph -> ps ) )
Assertion	spimed	|- ( ch -> ( ph -> E. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		spimed.1	|- ( ch -> F/ x ph )
2		spimed.2	|- ( x = y -> ( ph -> ps ) )
3	1	nf5rd	|- ( ch -> ( ph -> A. x ph ) )
4		ax6e	|- E. x x = y
5	4 2	eximii	|- E. x ( ph -> ps )
6	5	19.35i	|- ( A. x ph -> E. x ps )
7	3 6	syl6	|- ( ch -> ( ph -> E. x ps ) )