Metamath Proof Explorer

Theorem r19.29d2rOLD

Description: Obsolete version of r19.29d2r as of 4-Nov-2024. (Contributed by Thierry Arnoux, 30-Jan-2017) (New usage is discouraged.) (Proof modification is discouraged.)

		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.29d2rOLD	$⊢ φ \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		r19.29	$⊢ (\forall x \in A \forall y \in B ψ \land \exists x \in A \exists y \in B χ) \to \exists x \in A (\forall y \in B ψ \land \exists y \in B χ)$
4	1 2 3	syl2anc	$⊢ φ \to \exists x \in A (\forall y \in B ψ \land \exists y \in B χ)$
5		r19.29	$⊢ (\forall y \in B ψ \land \exists y \in B χ) \to \exists y \in B (ψ \land χ)$
6	5	reximi	$⊢ \exists x \in A (\forall y \in B ψ \land \exists y \in B χ) \to \exists x \in A \exists y \in B (ψ \land χ)$
7	4 6	syl	$⊢ φ \to \exists x \in A \exists y \in B (ψ \land χ)$