Theorem bj-sylget2

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

	Ref	Expression
Assertion	bj-sylget2	⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ( ∃ 𝑥 𝜓 → 𝜒 ) ) → ( ∃ 𝑥 𝜑 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-sylget	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ( ∃ 𝑥 𝜓 → 𝜒 ) → ( ∃ 𝑥 𝜑 → 𝜒 ) ) )
2	1	imp	⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ( ∃ 𝑥 𝜓 → 𝜒 ) ) → ( ∃ 𝑥 𝜑 → 𝜒 ) )