Theorem
19.21bi
Inference form of
19.21
and also deduction form of
sp
. (Contributed by NM, 26-May-1993.)
Hypothesis
19.21bi.1
\( \vdash \varphi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
19.21bi.1
\( \vdash \varphi \rightarrow \forall x \, \psi \)
sp
\( \vdash \forall x \, \psi \rightarrow \psi \)
syl
l0
_
This is the content in the right pane.