Theorem hbalw

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.)

Hypotheses
hbalw.1
\( \vdash x = z \rightarrow (\varphi \leftrightarrow \psi) \)
hbalw.2
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
Conclusion
\( \vdash \forall y \, \varphi \rightarrow \forall x \, \forall y \, \varphi \)
Proof
hbalw.2
l1
alimi _
\( \vdash \forall y \, \varphi \rightarrow \forall y \, \forall x \, \varphi \)
hbalw.1
\( \vdash x = z \rightarrow (\varphi \leftrightarrow \psi) \)
alcomimw _
\( \vdash \forall y \, \forall x \, \varphi \rightarrow \forall x \, \forall y \, \varphi \)
syl l1 _