Metamath Proof Explorer


Theorem exlimim

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

Ref Expression
Assertion exlimim x φ x φ ψ ψ

Proof

Step Hyp Ref Expression
1 nfa1 x x φ ψ
2 nfv x ψ
3 sp x φ ψ φ ψ
4 1 2 3 exlimd x φ ψ x φ ψ
5 4 impcom x φ x φ ψ ψ