Metamath Proof Explorer

Theorem rexlimivw

Description: Weaker version of rexlimiv . (Contributed by FL, 19-Sep-2011) (Proof shortened by Wolf Lammen, 23-Dec-2024)

Ref Expression
Hypothesis rexlimivw.1 
|- ( ph -> ps )
Assertion rexlimivw 
|- ( E. x e. A ph -> ps )

Proof

Step Hyp Ref Expression
1 rexlimivw.1 
 |-  ( ph -> ps )
2 1 adantl 
 |-  ( ( x e. A /\ ph ) -> ps )
3 2 rexlimiva 
 |-  ( E. x e. A ph -> ps )