Metamath Proof Explorer

Theorem r19.29d2r

Description: Theorem 19.29 of Margaris p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017) (Proof shortened by Wolf Lammen, 4-Nov-2024)

	Ref	Expression
Hypotheses	r19.29d2r.1	$⊢ φ \to \forall x \in A \forall y \in B ψ$
	r19.29d2r.2	$⊢ φ \to \exists x \in A \exists y \in B χ$
Assertion	r19.29d2r	$⊢ φ \to \exists x \in A \exists y \in B (ψ \land χ)$

Proof

Step	Hyp	Ref	Expression
1		r19.29d2r.1	$⊢ φ \to \forall x \in A \forall y \in B ψ$
2		r19.29d2r.2	$⊢ φ \to \exists x \in A \exists y \in B χ$
3		2r19.29	$⊢ (\forall x \in A \forall y \in B ψ \land \exists x \in A \exists y \in B χ) \to \exists x \in A \exists y \in B (ψ \land χ)$
4	1 2 3	syl2anc	$⊢ φ \to \exists x \in A \exists y \in B (ψ \land χ)$