This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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)

Ref Expression
Assertion 2stdpc4 ⊢ ∀ x ∀ y φ → z x w y φ

Proof

Step Hyp Ref Expression
1 stdpc4 ⊢ ∀ y φ → w y φ
2 1 alimi ⊢ ∀ x ∀ y φ → ∀ x w y φ
3 stdpc4 ⊢ ∀ x w y φ → z x w y φ
4 2 3 syl ⊢ ∀ x ∀ y φ → z x w y φ