Theorem axial

The setvar \( x \) is not free in \( \forall x \, \varphi \) (intuitionistic logic axiom ax-ial). (Contributed by Jim Kingdon, 31-Dec-2017.) (New usage is discouraged.)

Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall x \, \forall x \, \varphi \)
Proof
hba1