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 | |- ( A. x A. y ph -> [ z / x ] [ w / y ] ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | stdpc4 | |- ( A. y ph -> [ w / y ] ph ) |
|
| 2 | 1 | alimi | |- ( A. x A. y ph -> A. x [ w / y ] ph ) |
| 3 | stdpc4 | |- ( A. x [ w / y ] ph -> [ z / x ] [ w / y ] ph ) |
|
| 4 | 2 3 | syl | |- ( A. x A. y ph -> [ z / x ] [ w / y ] ph ) |