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

Metamath Proof Explorer

Theorem spimed

Description: Deduction version of spime . (Contributed by NM, 14-May-1993) (Revised by Mario Carneiro, 3-Oct-2016) (Proof shortened by Wolf Lammen, 19-Feb-2018) Usage of this theorem is discouraged because it depends on ax-13 . Use spimedv instead. (New usage is discouraged.)

	Ref	Expression
Hypotheses	spimed.1	$⊢ χ \to Ⅎ x φ$
	spimed.2	$⊢ x = y \to (φ \to ψ)$
Assertion	spimed	$⊢ χ \to (φ \to \exists x ψ)$

Proof

Step	Hyp	Ref	Expression
1		spimed.1	$⊢ χ \to Ⅎ x φ$
2		spimed.2	$⊢ x = y \to (φ \to ψ)$
3	1	nf5rd	$⊢ χ \to (φ \to \forall x φ)$
4		ax6e	$⊢ \exists x x = y$
5	4 2	eximii	$⊢ \exists x (φ \to ψ)$
6	5	19.35i	$⊢ \forall x φ \to \exists x ψ$
7	3 6	syl6	$⊢ χ \to (φ \to \exists x ψ)$