Theorem hbimd

Deduction form of bound-variable hypothesis builder hbim. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)

Hypotheses
hbimd.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
hbimd.2
\( \vdash \varphi \rightarrow \psi \rightarrow \forall x \, \psi \)
hbimd.3
\( \vdash \varphi \rightarrow \chi \rightarrow \forall x \, \chi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \rightarrow \chi) \rightarrow \forall x \, (\psi \rightarrow \chi) \)
Proof
l0
hbimd.1
hbimd.2
l2
nf5dh l0 _
l3
hbimd.1
hbimd.3
nf5dh l3 _
nfimd l2 _
nf5rd _