Metamath Proof Explorer

Theorem 19.29r

Description: Variation of 19.29 . (Contributed by NM, 18-Aug-1993) (Proof shortened by Wolf Lammen, 12-Nov-2020)

Ref Expression
Assertion 19.29r 
|- ( ( E. x ph /\ A. x ps ) -> E. x ( ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 pm3.21 
 |-  ( ps -> ( ph -> ( ph /\ ps ) ) )
2 1 aleximi 
 |-  ( A. x ps -> ( E. x ph -> E. x ( ph /\ ps ) ) )
3 2 impcom 
 |-  ( ( E. x ph /\ A. x ps ) -> E. x ( ph /\ ps ) )