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

Metamath Proof Explorer

Theorem hbalw

Description: Weak version of hbal . Uses only Tarski's FOL axiom schemes. Unlike hbal , this theorem requires that x and y be distinct, i.e., not be bundled. (Contributed by NM, 19-Apr-2017)

Ref Expression
Hypotheses hbalw.1 ⊢ x = z → φ ↔ ψ
hbalw.2 ⊢ φ → ∀ x φ
Assertion hbalw ⊢ ∀ y φ → ∀ x ∀ y φ

Proof

Step Hyp Ref Expression
1 hbalw.1 ⊢ x = z → φ ↔ ψ
2 hbalw.2 ⊢ φ → ∀ x φ
3 2 alimi ⊢ ∀ y φ → ∀ y ∀ x φ
4 1 alcomimw ⊢ ∀ y ∀ x φ → ∀ x ∀ y φ
5 3 4 syl ⊢ ∀ y φ → ∀ x ∀ y φ