Metamath Proof Explorer


Theorem exlimim

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

Ref Expression
Assertion exlimim ( ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝜑𝜓 ) ) → 𝜓 )

Proof

Step Hyp Ref Expression
1 nfa1 𝑥𝑥 ( 𝜑𝜓 )
2 nfv 𝑥 𝜓
3 sp ( ∀ 𝑥 ( 𝜑𝜓 ) → ( 𝜑𝜓 ) )
4 1 2 3 exlimd ( ∀ 𝑥 ( 𝜑𝜓 ) → ( ∃ 𝑥 𝜑𝜓 ) )
5 4 impcom ( ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝜑𝜓 ) ) → 𝜓 )