Description: Deduction form of Theorem 19.23 of Margaris p. 90, see 19.23 . (Contributed by NM, 27-Apr-1994) Remove dependencies on ax-6 , ax-7 . (Revised by Wolf Lammen, 4-Dec-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | exlimdv.1 | |- ( ph -> ( ps -> ch ) ) |
|
| Assertion | exlimdv | |- ( ph -> ( E. x ps -> ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exlimdv.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | 1 | eximdv | |- ( ph -> ( E. x ps -> E. x ch ) ) |
| 3 | ax5e | |- ( E. x ch -> ch ) |
|
| 4 | 2 3 | syl6 | |- ( ph -> ( E. x ps -> ch ) ) |