spimt

Description: Closed theorem form of spim . (Contributed by NM, 15-Jan-2008) (Revised by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 21-Mar-2023) Usage of this theorem is discouraged because it depends on ax-13 . (New usage is discouraged.)

		Ref	Expression
	Assertion	spimt	$⊢ (Ⅎ x ψ \land \forall x (x = y \to (φ \to ψ))) \to (\forall x φ \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		ax6e	$⊢ \exists x x = y$
2		exim	$⊢ \forall x (x = y \to (φ \to ψ)) \to (\exists x x = y \to \exists x (φ \to ψ))$
3	1 2	mpi	$⊢ \forall x (x = y \to (φ \to ψ)) \to \exists x (φ \to ψ)$
4		19.35	$⊢ \exists x (φ \to ψ) \leftrightarrow (\forall x φ \to \exists x ψ)$
5	3 4	sylib	$⊢ \forall x (x = y \to (φ \to ψ)) \to (\forall x φ \to \exists x ψ)$
6		id	$⊢ Ⅎ x ψ \to Ⅎ x ψ$
7	6	19.9d	$⊢ Ⅎ x ψ \to (\exists x ψ \to ψ)$
8	5 7	sylan9r	$⊢ (Ⅎ x ψ \land \forall x (x = y \to (φ \to ψ))) \to (\forall x φ \to ψ)$

Metamath Proof Explorer

Theorem spimt

Proof