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	|- ( ph -> A. y ps )
	bj-hbexd.maj	|- ( ps -> ( ch -> A. x th ) )
Assertion	bj-hbexd	|- ( ph -> ( E. y ch -> A. x E. y th ) )

Proof

Step	Hyp	Ref	Expression
1		bj-hbexd.nf	|- ( ph -> A. y ps )
2		bj-hbexd.maj	|- ( ps -> ( ch -> A. x th ) )
3		19.12	|- ( E. y A. x th -> A. x E. y th )
4	3	a1i	|- ( ph -> ( E. y A. x th -> A. x E. y th ) )
5	1 4 2	bj-exlimd	|- ( ph -> ( E. y ch -> A. x E. y th ) )