Theorem 2sp

A double specialization (see sp ). Another double specialization, closer to PM*11.1, is 2stdpc4. (Contributed by BJ, 15-Sep-2018.)

Conclusion
\( \vdash \forall x \, \forall y \, \varphi \rightarrow \varphi \)
Proof
sp
sps _