Theorem pm11.11

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

	Ref	Expression
Hypothesis	pm11.11.1	|- ph
Assertion	pm11.11	|- A. z A. w [ z / x ] [ w / y ] ph

Proof

Step	Hyp	Ref	Expression
1		pm11.11.1	|- ph
2		2stdpc4	|- ( A. x A. y ph -> [ z / x ] [ w / y ] ph )
3	1	ax-gen	|- A. y ph
4	2 3	mpg	|- [ z / x ] [ w / y ] ph
5	4	gen2	|- A. z A. w [ z / x ] [ w / y ] ph