Theorem axi5r

Converse of axc4 (intuitionistic logic axiom ax-i5r). (Contributed by Jim Kingdon, 31-Dec-2017.)

Conclusion
\( \vdash (\forall x \, \varphi \rightarrow \forall x \, \psi) \rightarrow \forall x \, (\forall x \, \varphi \rightarrow \psi) \)
Proof
l0
hba1
hba1
l2
hbim l0 _
sp
imim2i _
alrimih l2 _