Metamath Proof Explorer

Theorem bj-nexdh

Description: Closed form of nexdh (actually, its general instance). (Contributed by BJ, 6-May-2019)

Ref Expression
Assertion bj-nexdh 
|- ( A. x ( ph -> -. ps ) -> ( ( ch -> A. x ph ) -> ( ch -> -. E. x ps ) ) )

Proof

Step Hyp Ref Expression
1 sylgt 
 |-  ( A. x ( ph -> -. ps ) -> ( ( ch -> A. x ph ) -> ( ch -> A. x -. ps ) ) )
2 alnex 
 |-  ( A. x -. ps <-> -. E. x ps )
3 1 2 syl8ib 
 |-  ( A. x ( ph -> -. ps ) -> ( ( ch -> A. x ph ) -> ( ch -> -. E. x ps ) ) )