Theorem hbim

If \( x \) is not free in \( \varphi \) and \( \psi \), it is not free in \( \varphi \rightarrow \psi \). (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 3-Mar-2008.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)

Hypotheses
hbim.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
hbim.2
\( \vdash \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow \forall x \, (\varphi \rightarrow \psi) \)
Proof
l0
hbim.1
hbim.2
a1i _
hbim1 l0 _