Description: Inference from existential specialization. (Contributed by NM, 19-Aug-1993) (Revised by Wolf Lammen, 22-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | speiv.1 | |- ( x = y -> ( ps -> ph ) ) |
|
speiv.2 | |- ps |
||
Assertion | speiv | |- E. x ph |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | speiv.1 | |- ( x = y -> ( ps -> ph ) ) |
|
2 | speiv.2 | |- ps |
|
3 | 2 | hbth | |- ( ps -> A. x ps ) |
4 | 3 1 | spimew | |- ( ps -> E. x ph ) |
5 | 2 4 | ax-mp | |- E. x ph |