Description: Weak version of 19.8a and instance of 19.2d . (Contributed by NM, 1-Aug-2017) (Proof shortened by Wolf Lammen, 4-Dec-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | 19.8w.1 | ⊢ ( 𝜑 → ∀ 𝑥 𝜑 ) | |
| Assertion | 19.8w | ⊢ ( 𝜑 → ∃ 𝑥 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.8w.1 | ⊢ ( 𝜑 → ∀ 𝑥 𝜑 ) | |
| 2 | 1 | 19.2d | ⊢ ( 𝜑 → ∃ 𝑥 𝜑 ) |