Theorem pm11.11

Description: Theorem *11.11 in WhiteheadRussell p. 159. (Contributed by Andrew Salmon, 17-Jun-2011)

	Ref	Expression
Hypothesis	pm11.11.1	$$⊢\phi$$
Assertion	pm11.11	$$⊢\forall z\forall w\left[z/x\right]\left[w/y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		pm11.11.1	$$⊢\phi$$
2		2stdpc4	$$⊢\forall x\forall y\phi \to \left[z/x\right]\left[w/y\right]\phi$$
3	1	ax-gen	$$⊢\forall y\phi$$
4	2 3	mpg	$$⊢\left[z/x\right]\left[w/y\right]\phi$$
5	4	gen2	$$⊢\forall z\forall w\left[z/x\right]\left[w/y\right]\phi$$