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

Metamath Proof Explorer

Theorem exlimdv

Description: Deduction form of Theorem 19.23 of Margaris p. 90, see 19.23 . (Contributed by NM, 27-Apr-1994) Remove dependencies on ax-6 , ax-7 . (Revised by Wolf Lammen, 4-Dec-2017)

		Ref	Expression
	Hypothesis	exlimdv.1	$⊢ φ \to (ψ \to χ)$
	Assertion	exlimdv	$⊢ φ \to (\exists x ψ \to χ)$

Proof

Step	Hyp	Ref	Expression
1		exlimdv.1	$⊢ φ \to (ψ \to χ)$
2	1	eximdv	$⊢ φ \to (\exists x ψ \to \exists x χ)$
3		ax5e	$⊢ \exists x χ \to χ$
4	2 3	syl6	$⊢ φ \to (\exists x ψ \to χ)$