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

Metamath Proof Explorer

Theorem hbalg

Description: Closed form of hbal . Derived from hbalgVD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion hbalg ⊢ ∀ y φ → ∀ x φ → ∀ y ∀ 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 φ
4 3 axc4i ⊢ ∀ y φ → ∀ x φ → ∀ y ∀ y φ → ∀ x ∀ y φ