Metamath Proof Explorer


Theorem reximddv3

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 )

Proof

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 )