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

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	1 2	jca	$⊢ φ \to (\forall x \in A \forall y \in B ψ \land \exists x \in A \exists y \in B χ)$
4		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 χ)$
5	3 4	syl	$⊢ φ \to \exists x \in A \exists y \in B (ψ \land χ)$