Theorem pm11.11

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

	Ref	Expression
Hypothesis	pm11.11.1	⊢ 𝜑
Assertion	pm11.11	⊢ ∀ 𝑧 ∀ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑

Proof

Step	Hyp	Ref	Expression
1		pm11.11.1	⊢ 𝜑
2		2stdpc4	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
3	1	ax-gen	⊢ ∀ 𝑦 𝜑
4	2 3	mpg	⊢ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑
5	4	gen2	⊢ ∀ 𝑧 ∀ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑