Description: Theorem *10.14 in WhiteheadRussell p. 146. (Contributed by Andrew Salmon, 17-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | pm10.14 | |- ( ( A. x ph /\ A. x ps ) -> ( [ y / x ] ph /\ [ y / x ] ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stdpc4 | |- ( A. x ph -> [ y / x ] ph ) |
|
2 | stdpc4 | |- ( A. x ps -> [ y / x ] ps ) |
|
3 | 1 2 | anim12i | |- ( ( A. x ph /\ A. x ps ) -> ( [ y / x ] ph /\ [ y / x ] ps ) ) |