Theorem bj-hbal

Description: More general instance of hbal . (Contributed by BJ, 4-Apr-2026)

	Ref	Expression
Hypothesis	bj-hbal.1	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
Assertion	bj-hbal	⊢ ( ∀ 𝑦 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		bj-hbal.1	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
2		bj-hbalt	⊢ ( ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜓 ) → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜓 ) )
3	2 1	mpg	⊢ ( ∀ 𝑦 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜓 )