Metamath Proof Explorer


Theorem exlimim

Description: Closed form of exlimimd . (Contributed by ML, 17-Jul-2020)

Ref Expression
Assertion exlimim
|- ( ( E. x ph /\ A. x ( ph -> ps ) ) -> ps )

Proof

Step Hyp Ref Expression
1 nfa1
 |-  F/ x A. x ( ph -> ps )
2 nfv
 |-  F/ x ps
3 sp
 |-  ( A. x ( ph -> ps ) -> ( ph -> ps ) )
4 1 2 3 exlimd
 |-  ( A. x ( ph -> ps ) -> ( E. x ph -> ps ) )
5 4 impcom
 |-  ( ( E. x ph /\ A. x ( ph -> ps ) ) -> ps )