Theorem bj-hbexd

Description: A more general instance of the deduction form of hbex . (Contributed by BJ, 4-Apr-2026)

	Ref	Expression
Hypotheses	bj-hbexd.nf	$$⊢\phi \to \forall y\psi$$
	bj-hbexd.maj	$$⊢\psi \to \left(\chi \to \forall x\theta \right)$$
Assertion	bj-hbexd	$$⊢\phi \to \left(\exists y\chi \to \forall x\exists y\theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-hbexd.nf	$$⊢\phi \to \forall y\psi$$
2		bj-hbexd.maj	$$⊢\psi \to \left(\chi \to \forall x\theta \right)$$
3		19.12	$$⊢\exists y\forall x\theta \to \forall x\exists y\theta$$
4	3	a1i	$$⊢\phi \to \left(\exists y\forall x\theta \to \forall x\exists y\theta \right)$$
5	1 4 2	bj-exlimd	$$⊢\phi \to \left(\exists y\chi \to \forall x\exists y\theta \right)$$