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

Metamath Proof Explorer

Theorem bj-hbalt

Description: Closed form of hbal . When in main part, prove hbal and hbald from it. (Contributed by BJ, 2-May-2019)

Ref Expression
Assertion bj-hbalt ⊢ ∀ y φ → ∀ x φ → ∀ y φ → ∀ x ∀ y φ

Proof

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