Metamath Proof Explorer


Theorem exinst

Description: Existential Instantiation. Virtual deduction form of exlimexi . (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses exinst.1 ψxψ
exinst.2 xφ,φψ
Assertion exinst xφψ

Proof

Step Hyp Ref Expression
1 exinst.1 ψxψ
2 exinst.2 xφ,φψ
3 2 dfvd2i xφφψ
4 1 3 exlimexi xφψ