Metamath Proof Explorer
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 |
|- ( ph -> A. x ph ) |
|
Assertion |
19.8w |
|- ( ph -> E. x ph ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
19.8w.1 |
|- ( ph -> A. x ph ) |
2 |
1
|
19.2d |
|- ( ph -> E. x ph ) |