Description: Weak version of sp . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017) (Proof shortened by Wolf Lammen, 13-Aug-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | spnfw.1 | |- ( -. ph -> A. x -. ph ) |
|
Assertion | spnfw | |- ( A. x ph -> ph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spnfw.1 | |- ( -. ph -> A. x -. ph ) |
|
2 | idd | |- ( x = y -> ( ph -> ph ) ) |
|
3 | 1 2 | spimw | |- ( A. x ph -> ph ) |