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

Metamath Proof Explorer

Theorem rexlimd2

Description: Version of rexlimd with deduction version of second hypothesis. (Contributed by NM, 21-Jul-2013) (Revised by Mario Carneiro, 8-Oct-2016)

	Ref	Expression
Hypotheses	rexlimd2.1	$⊢ Ⅎ x φ$
	rexlimd2.2	$⊢ φ \to Ⅎ x χ$
	rexlimd2.3	$⊢ φ \to (x \in A \to (ψ \to χ))$
Assertion	rexlimd2	$⊢ φ \to (\exists x \in A ψ \to χ)$

Proof

Step	Hyp	Ref	Expression
1		rexlimd2.1	$⊢ Ⅎ x φ$
2		rexlimd2.2	$⊢ φ \to Ⅎ x χ$
3		rexlimd2.3	$⊢ φ \to (x \in A \to (ψ \to χ))$
4	1 3	ralrimi	$⊢ φ \to \forall x \in A (ψ \to χ)$
5		r19.23t	$⊢ Ⅎ x χ \to (\forall x \in A (ψ \to χ) \leftrightarrow (\exists x \in A ψ \to χ))$
6	2 5	syl	$⊢ φ \to (\forall x \in A (ψ \to χ) \leftrightarrow (\exists x \in A ψ \to χ))$
7	4 6	mpbid	$⊢ φ \to (\exists x \in A ψ \to χ)$