Theorem bj-spim0

Description: A universal specialization result in deduction form, proved 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-spim0.nf0	$$⊢\phi \to \forall x\phi$$
	bj-spim0.nf	$$⊢\phi \to \left(\exists x\chi \to \chi \right)$$
	bj-spim0.is	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \to \chi \right)$$
Assertion	bj-spim0	$$⊢\phi \to \left(\forall x\psi \to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-spim0.nf0	$$⊢\phi \to \forall x\phi$$
2		bj-spim0.nf	$$⊢\phi \to \left(\exists x\chi \to \chi \right)$$
3		bj-spim0.is	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \to \chi \right)$$
4		ax6ev	$$⊢\exists xx=y$$
5	4	a1i	$$⊢\phi \to \exists xx=y$$
6	1 2 5 3	bj-spim	$$⊢\phi \to \left(\forall x\psi \to \chi \right)$$