Theorem bj-nnf-spime

Description: An existential generalization result in deduction form, from ax-1 -- ax-6 , where the only DV condition is on x , y , and where x should be nonfree in the new proposition ch (and in the context ph ). (Contributed by BJ, 4-Apr-2026)

	Ref	Expression
Hypotheses	bj-nnf-spime.nf0	|- ( ph -> A. x ph )
	bj-nnf-spime.nf	|- ( ph -> F// x ps )
	bj-nnf-spime.is	|- ( ( ph /\ x = y ) -> ( ps -> ch ) )
Assertion	bj-nnf-spime	|- ( ph -> ( ps -> E. x ch ) )

Proof

Step	Hyp	Ref	Expression
1		bj-nnf-spime.nf0	|- ( ph -> A. x ph )
2		bj-nnf-spime.nf	|- ( ph -> F// x ps )
3		bj-nnf-spime.is	|- ( ( ph /\ x = y ) -> ( ps -> ch ) )
4		ax6ev	|- E. x x = y
5	3	ex	|- ( ph -> ( x = y -> ( ps -> ch ) ) )
6	1 5	eximdh	|- ( ph -> ( E. x x = y -> E. x ( ps -> ch ) ) )
7	4 6	mpi	|- ( ph -> E. x ( ps -> ch ) )
8		bj-19.37im	|- ( F// x ps -> ( E. x ( ps -> ch ) -> ( ps -> E. x ch ) ) )
9	2 7 8	sylc	|- ( ph -> ( ps -> E. x ch ) )