Theorem hbal

If \( x \) is not free in \( \varphi \), it is not free in \( \forall y \, \varphi \). (Contributed by NM, 12-Mar-1993.)

Hypothesis
hbal.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
Conclusion
\( \vdash \forall y \, \varphi \rightarrow \forall x \, \forall y \, \varphi \)
Proof
hbal.1
l1
alimi _
\( \vdash \forall y \, \varphi \rightarrow \forall y \, \forall x \, \varphi \)
ax-11
\( \vdash \forall y \, \forall x \, \varphi \rightarrow \forall x \, \forall y \, \varphi \)
syl l1 _