Theorem rexlim2d

Description: Inference removing two restricted quantifiers. Same as rexlimdvv , but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	rexlim2d.x	⊢ Ⅎ 𝑥 𝜑
	rexlim2d.y	⊢ Ⅎ 𝑦 𝜑
	rexlim2d.3	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝜓 → 𝜒 ) ) )
Assertion	rexlim2d	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		rexlim2d.x	⊢ Ⅎ 𝑥 𝜑
2		rexlim2d.y	⊢ Ⅎ 𝑦 𝜑
3		rexlim2d.3	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝜓 → 𝜒 ) ) )
4		nfv	⊢ Ⅎ 𝑥 𝜒
5		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
6	2 5	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ 𝐴 )
7		nfv	⊢ Ⅎ 𝑦 𝜒
8	3	expdimp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ( 𝜓 → 𝜒 ) ) )
9	6 7 8	rexlimd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐵 𝜓 → 𝜒 ) )
10	9	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 𝜓 → 𝜒 ) ) )
11	1 4 10	rexlimd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → 𝜒 ) )