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	$$⊢\phi \to \forall x\phi$$
	bj-nnf-spime.nf	$$⊢\phi \to Ⅎ\text{'}x\psi$$
	bj-nnf-spime.is	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \to \chi \right)$$
Assertion	bj-nnf-spime	$$⊢\phi \to \left(\psi \to \exists x\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-nnf-spime.nf0	$$⊢\phi \to \forall x\phi$$
2		bj-nnf-spime.nf	$$⊢\phi \to Ⅎ\text{'}x\psi$$
3		bj-nnf-spime.is	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \to \chi \right)$$
4		ax6ev	$$⊢\exists xx=y$$
5	3	ex	$$⊢\phi \to \left(x=y\to \left(\psi \to \chi \right)\right)$$
6	1 5	eximdh	$$⊢\phi \to \left(\exists xx=y\to \exists x\left(\psi \to \chi \right)\right)$$
7	4 6	mpi	$$⊢\phi \to \exists x\left(\psi \to \chi \right)$$
8		bj-19.37im	$$⊢Ⅎ\text{'}x\psi \to \left(\exists x\left(\psi \to \chi \right)\to \left(\psi \to \exists x\chi \right)\right)$$
9	2 7 8	sylc	$$⊢\phi \to \left(\psi \to \exists x\chi \right)$$