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 ⊢ ∀ x φ → ∀ y ψ → ∀ x φ → ∀ y ∀ x ψ

Proof

Step Hyp Ref Expression
1 alim ⊢ ∀ x φ → ∀ y ψ → ∀ x φ → ∀ x ∀ y ψ
2 ax-11 ⊢ ∀ x ∀ y ψ → ∀ y ∀ x ψ
3 1 2 syl6 ⊢ ∀ x φ → ∀ y ψ → ∀ x φ → ∀ y ∀ x ψ