# 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}\to \left({\phi }↔{\psi }\right)$
hbalw.2 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion hbalw ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 hbalw.1 ${⊢}{x}={z}\to \left({\phi }↔{\psi }\right)$
2 hbalw.2 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 2 alimi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
4 1 alcomiw ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
5 3 4 syl ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$