Theorem r19.29vva

Description: A commonly used pattern based on r19.29 , version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017) (Proof shortened by Wolf Lammen, 29-Jun-2023)

	Ref	Expression
Hypotheses	r19.29vva.1	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → 𝜒 )
	r19.29vva.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
Assertion	r19.29vva	⊢ ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		r19.29vva.1	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → 𝜒 )
2		r19.29vva.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
3	1 2	reximddv2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜒 )
4		id	⊢ ( 𝜒 → 𝜒 )
5	4	rexlimivw	⊢ ( ∃ 𝑦 ∈ 𝐵 𝜒 → 𝜒 )
6	5	reximi	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜒 → ∃ 𝑥 ∈ 𝐴 𝜒 )
7	4	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜒 → 𝜒 )
8	3 6 7	3syl	⊢ ( 𝜑 → 𝜒 )