Theorem hbnd

Deduction form of bound-variable hypothesis builder hbn. (Contributed by NM, 3-Jan-2002.)

Hypotheses
hbnd.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
hbnd.2
\( \vdash \varphi \rightarrow \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \forall x \, \neg \psi \)
Proof
l0
hbnd.1
hbnd.2
l2
alrimih l0 _
\( \vdash \varphi \rightarrow \forall x \, (\psi \rightarrow \forall x \, \psi) \)
hbnt
\( \vdash \forall x \, (\psi \rightarrow \forall x \, \psi) \rightarrow \neg \psi \rightarrow \forall x \, \neg \psi \)
syl l2 _