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 ) |