Theorem hbald
Deduction form of bound-variable hypothesis builder hbal.
(Contributed by NM, 2-Jan-2002.)
Hypotheses
hbald.1
\( \vdash \varphi \rightarrow \forall y \, \varphi \)
hbald.2
\( \vdash \varphi \rightarrow \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \forall y \, \psi \rightarrow \forall x \, \forall y \, \psi \)
Proof
l0
hbald.1
hbald.2
l2
alimdh l0 _
\( \vdash \varphi \rightarrow \forall y \, \psi \rightarrow \forall y \, \forall x \, \psi \)
ax-11
\( \vdash \forall y \, \forall x \, \psi \rightarrow \forall x \, \forall y \, \psi \)
syl6 l2 _