This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \forall x (χ \to φ) \to ((\exists x φ \to ψ) \to (\exists x χ \to ψ))$

Step	Hyp	Ref	Expression
1		exim	$⊢ \forall x (χ \to φ) \to (\exists x χ \to \exists x φ)$
2	1	imim1d	$⊢ \forall x (χ \to φ) \to ((\exists x φ \to ψ) \to (\exists x χ \to ψ))$