This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜓 ) )