Description: Inference from Theorem 19.23 of Margaris p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | rexlimiv.1 | |- ( x e. A -> ( ph -> ps ) ) |
|
| Assertion | rexlimiv | |- ( E. x e. A ph -> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rexlimiv.1 | |- ( x e. A -> ( ph -> ps ) ) |
|
| 2 | 1 | imp | |- ( ( x e. A /\ ph ) -> ps ) |
| 3 | 2 | rexlimiva | |- ( E. x e. A ph -> ps ) |