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

Metamath Proof Explorer

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, 4-Nov-2024)

	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		idd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝜒 → 𝜒 ) )
5	4	rexlimivv	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜒 → 𝜒 )
6	3 5	syl	⊢ ( 𝜑 → 𝜒 )