Theorem hbim1

A closed form of hbim. (Contributed by NM, 2-Jun-1993.)

Hypotheses
hbim1.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
hbim1.2
\( \vdash \varphi \rightarrow \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow \forall x \, (\varphi \rightarrow \psi) \)
Proof
hbim1.2
l1
a2i _
\( \vdash (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \forall x \, \psi \)
hbim1.1
19.21h _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \forall x \, \psi \)
sylibr l1 _