Metamath Proof Explorer


Theorem speiv

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

Proof

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