Metamath Proof Explorer

Theorem r19.29r

Description: Restricted quantifier version of 19.29r ; variation of r19.29 . (Contributed by NM, 31-Aug-1999) (Proof shortened by Wolf Lammen, 29-Jun-2023)

		Ref	Expression
	Assertion	r19.29r	$⊢ (\exists x \in A φ \land \forall x \in A ψ) \to \exists x \in A (φ \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		r19.29	$⊢ (\forall x \in A ψ \land \exists x \in A φ) \to \exists x \in A (ψ \land φ)$
2	1	ancoms	$⊢ (\exists x \in A φ \land \forall x \in A ψ) \to \exists x \in A (ψ \land φ)$
3		pm3.22	$⊢ (ψ \land φ) \to (φ \land ψ)$
4	3	reximi	$⊢ \exists x \in A (ψ \land φ) \to \exists x \in A (φ \land ψ)$
5	2 4	syl	$⊢ (\exists x \in A φ \land \forall x \in A ψ) \to \exists x \in A (φ \land ψ)$