Theorem 2stdpc4

A double specialization using explicit substitution. This is Theorem PM*11.1 in [WhiteheadRussell] p. 159. See stdpc4 for the analogous single specialization. See 2sp for another double specialization. (Contributed by Andrew Salmon, 24-May-2011.)

Conclusion
\( \vdash \forall x \, \forall y \, \varphi \rightarrow [ z' / x ] \, [ w' / y ] \, \varphi \)
Proof
stdpc4
l1
alimi _
\( \vdash \forall x \, \forall y \, \varphi \rightarrow \forall x \, [ w' / y ] \, \varphi \)
stdpc4
\( \vdash \forall x \, [ w' / y ] \, \varphi \rightarrow [ z' / x ] \, [ w' / y ] \, \varphi \)
syl l1 _