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	⊢ Ⅎ 𝑥 𝜑
	rexlimd2.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
	rexlimd2.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) )
Assertion	rexlimd2	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		rexlimd2.1	⊢ Ⅎ 𝑥 𝜑
2		rexlimd2.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
3		rexlimd2.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) )
4	1 3	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) )
5		r19.23t	⊢ ( Ⅎ 𝑥 𝜒 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) ) )
6	2 5	syl	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) ) )
7	4 6	mpbid	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) )