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	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		stdpc4	⊢ ( ∀ 𝑦 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 )
2	1	alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑥 [ 𝑤 / 𝑦 ] 𝜑 )
3		stdpc4	⊢ ( ∀ 𝑥 [ 𝑤 / 𝑦 ] 𝜑 → [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
4	2 3	syl	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )