Theorem bj-hbald

Description: General statement that hbald proves . (Contributed by BJ, 4-Apr-2026)

	Ref	Expression
Hypotheses	bj-hbald.1	⊢ ( 𝜑 → ∀ 𝑦 𝜓 )
	bj-hbald.2	⊢ ( 𝜓 → ( 𝜒 → ∀ 𝑥 𝜃 ) )
Assertion	bj-hbald	⊢ ( 𝜑 → ( ∀ 𝑦 𝜒 → ∀ 𝑥 ∀ 𝑦 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-hbald.1	⊢ ( 𝜑 → ∀ 𝑦 𝜓 )
2		bj-hbald.2	⊢ ( 𝜓 → ( 𝜒 → ∀ 𝑥 𝜃 ) )
3	2	al2imi	⊢ ( ∀ 𝑦 𝜓 → ( ∀ 𝑦 𝜒 → ∀ 𝑦 ∀ 𝑥 𝜃 ) )
4	1 3	syl	⊢ ( 𝜑 → ( ∀ 𝑦 𝜒 → ∀ 𝑦 ∀ 𝑥 𝜃 ) )
5		ax-11	⊢ ( ∀ 𝑦 ∀ 𝑥 𝜃 → ∀ 𝑥 ∀ 𝑦 𝜃 )
6	4 5	syl6	⊢ ( 𝜑 → ( ∀ 𝑦 𝜒 → ∀ 𝑥 ∀ 𝑦 𝜃 ) )