Description: Closed theorem form of spim . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Jan-2008) (Revised by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 21-Mar-2023) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | spimt | ⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) ) → ( ∀ 𝑥 𝜑 → 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax6e | ⊢ ∃ 𝑥 𝑥 = 𝑦 | |
| 2 | exim | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) → ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ( 𝜑 → 𝜓 ) ) ) | |
| 3 | 1 2 | mpi | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) → ∃ 𝑥 ( 𝜑 → 𝜓 ) ) |
| 4 | 19.35 | ⊢ ( ∃ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) | |
| 5 | 3 4 | sylib | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) → ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) ) |
| 6 | id | ⊢ ( Ⅎ 𝑥 𝜓 → Ⅎ 𝑥 𝜓 ) | |
| 7 | 6 | 19.9d | ⊢ ( Ⅎ 𝑥 𝜓 → ( ∃ 𝑥 𝜓 → 𝜓 ) ) |
| 8 | 5 7 | sylan9r | ⊢ ( ( Ⅎ 𝑥 𝜓 ∧ ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) ) → ( ∀ 𝑥 𝜑 → 𝜓 ) ) |