Metamath Proof Explorer

Theorem bj-sylgt2

Description: Uncurried (imported) form of sylgt . (Contributed by BJ, 2-May-2019)

Ref Expression
Assertion bj-sylgt2 
|- ( ( A. x ( ps -> ch ) /\ ( ph -> A. x ps ) ) -> ( ph -> A. x ch ) )

Proof

Step Hyp Ref Expression
1 sylgt 
 |-  ( A. x ( ps -> ch ) -> ( ( ph -> A. x ps ) -> ( ph -> A. x ch ) ) )
2 1 imp 
 |-  ( ( A. x ( ps -> ch ) /\ ( ph -> A. x ps ) ) -> ( ph -> A. x ch ) )