Theorem bj-sylget2

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

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

Proof

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