Description: Theorem close to a closed form of spnfw . (Contributed by BJ, 12-May-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-spnfw | |- ( ( E. x ph -> ps ) -> ( A. x ph -> ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.2 | |- ( A. x ph -> E. x ph ) |
|
2 | 1 | imim1i | |- ( ( E. x ph -> ps ) -> ( A. x ph -> ps ) ) |