Theorem rexlimd3

Description: * Inference from Theorem 19.23 of Margaris p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	rexlimd3.1	⊢ Ⅎ 𝑥 𝜑
	rexlimd3.2	⊢ Ⅎ 𝑥 𝜒
	rexlimd3.3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
Assertion	rexlimd3	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		rexlimd3.1	⊢ Ⅎ 𝑥 𝜑
2		rexlimd3.2	⊢ Ⅎ 𝑥 𝜒
3		rexlimd3.3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
4	3	exp31	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) )
5	1 2 4	rexlimd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) )