Description: Deduction from Theorem 19.22 of Margaris p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | reximddv3.1 | |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch ) |
|
reximddv3.2 | |- ( ph -> E. x e. A ps ) |
||
Assertion | reximddv3 | |- ( ph -> E. x e. A ch ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximddv3.1 | |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch ) |
|
2 | reximddv3.2 | |- ( ph -> E. x e. A ps ) |
|
3 | 1 | anasss | |- ( ( ph /\ ( x e. A /\ ps ) ) -> ch ) |
4 | 3 2 | reximddv | |- ( ph -> E. x e. A ch ) |