Description: Closed form of exlimimd . (Contributed by ML, 17-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | exlimim | ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) → 𝜓 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfa1 | ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝜑 → 𝜓 ) | |
2 | nfv | ⊢ Ⅎ 𝑥 𝜓 | |
3 | sp | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) | |
4 | 1 2 3 | exlimd | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → 𝜓 ) ) |
5 | 4 | impcom | ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) → 𝜓 ) |