Metamath Proof Explorer

Theorem bj-sylget

Description: Dual statement of sylgt . Closed form of bj-sylge . (Contributed by BJ, 2-May-2019)

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

Proof

Step Hyp Ref Expression
1 exim 
 |-  ( A. x ( ch -> ph ) -> ( E. x ch -> E. x ph ) )
2 1 imim1d 
 |-  ( A. x ( ch -> ph ) -> ( ( E. x ph -> ps ) -> ( E. x ch -> ps ) ) )