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	⊢ ( 𝜑 → ∀ 𝑦 𝜓 )
	bj-hbexd.maj	⊢ ( 𝜓 → ( 𝜒 → ∀ 𝑥 𝜃 ) )
Assertion	bj-hbexd	⊢ ( 𝜑 → ( ∃ 𝑦 𝜒 → ∀ 𝑥 ∃ 𝑦 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-hbexd.nf	⊢ ( 𝜑 → ∀ 𝑦 𝜓 )
2		bj-hbexd.maj	⊢ ( 𝜓 → ( 𝜒 → ∀ 𝑥 𝜃 ) )
3		19.12	⊢ ( ∃ 𝑦 ∀ 𝑥 𝜃 → ∀ 𝑥 ∃ 𝑦 𝜃 )
4	3	a1i	⊢ ( 𝜑 → ( ∃ 𝑦 ∀ 𝑥 𝜃 → ∀ 𝑥 ∃ 𝑦 𝜃 ) )
5	1 4 2	bj-exlimd	⊢ ( 𝜑 → ( ∃ 𝑦 𝜒 → ∀ 𝑥 ∃ 𝑦 𝜃 ) )