Theorem hbaltg

Description: A more general and closed form of hbal . (Contributed by Scott Fenton, 13-Dec-2010)

	Ref	Expression
Assertion	hbaltg	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		alim	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜓 ) )
2		ax-11	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜓 → ∀ 𝑦 ∀ 𝑥 𝜓 )
3	1 2	syl6	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜓 ) )