Theorem 2stdpc4

Description: 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) (Revised by BJ, 21-Oct-2018)

	Ref	Expression
Assertion	2stdpc4	$$⊢\forall x\forall y\phi \to \left[z/x\right]\left[w/y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		stdpc4	$$⊢\forall y\phi \to \left[w/y\right]\phi$$
2	1	alimi	$$⊢\forall x\forall y\phi \to \forall x\left[w/y\right]\phi$$
3		stdpc4	$$⊢\forall x\left[w/y\right]\phi \to \left[z/x\right]\left[w/y\right]\phi$$
4	2 3	syl	$$⊢\forall x\forall y\phi \to \left[z/x\right]\left[w/y\right]\phi$$