Metamath Proof Explorer

Theorem bj-spimt2

Description: A step in the proof of spimt . (Contributed by BJ, 2-May-2019)

		Ref	Expression
	Assertion	bj-spimt2	$⊢ \forall x (x = y \to (φ \to ψ)) \to ((\exists x ψ \to ψ) \to (\forall x φ \to ψ))$

Step	Hyp	Ref	Expression
1		bj-alequex	$⊢ \forall x (x = y \to (φ \to ψ)) \to \exists x (φ \to ψ)$
2		19.35	$⊢ \exists x (φ \to ψ) \leftrightarrow (\forall x φ \to \exists x ψ)$
3	1 2	sylib	$⊢ \forall x (x = y \to (φ \to ψ)) \to (\forall x φ \to \exists x ψ)$
4	3	imim1d	$⊢ \forall x (x = y \to (φ \to ψ)) \to ((\exists x ψ \to ψ) \to (\forall x φ \to ψ))$