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 ψ φ
speiv.2 ψ
Assertion speiv x φ

Proof

Step Hyp Ref Expression
1 speiv.1 x = y ψ φ
2 speiv.2 ψ
3 2 hbth ψ x ψ
4 3 1 spimew ψ x φ
5 2 4 ax-mp x φ