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 ( ∀ 𝑥 ( 𝜒𝜑 ) → ( ( ∃ 𝑥 𝜑𝜓 ) → ( ∃ 𝑥 𝜒𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 exim ( ∀ 𝑥 ( 𝜒𝜑 ) → ( ∃ 𝑥 𝜒 → ∃ 𝑥 𝜑 ) )
2 1 imim1d ( ∀ 𝑥 ( 𝜒𝜑 ) → ( ( ∃ 𝑥 𝜑𝜓 ) → ( ∃ 𝑥 𝜒𝜓 ) ) )