Theorem r19.29rOLD

Description: Obsolete version of r19.29r as of 22-Dec-2024. (Contributed by NM, 31-Aug-1999) (Proof shortened by Wolf Lammen, 29-Jun-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	r19.29rOLD	$$⊢\left(\exists x\in A\phi \wedge \forall x\in A\psi \right)\to \exists x\in A\left(\phi \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		r19.29	$$⊢\left(\forall x\in A\psi \wedge \exists x\in A\phi \right)\to \exists x\in A\left(\psi \wedge \phi \right)$$
2	1	ancoms	$$⊢\left(\exists x\in A\phi \wedge \forall x\in A\psi \right)\to \exists x\in A\left(\psi \wedge \phi \right)$$
3		pm3.22	$$⊢\left(\psi \wedge \phi \right)\to \left(\phi \wedge \psi \right)$$
4	3	reximi	$$⊢\exists x\in A\left(\psi \wedge \phi \right)\to \exists x\in A\left(\phi \wedge \psi \right)$$
5	2 4	syl	$$⊢\left(\exists x\in A\phi \wedge \forall x\in A\psi \right)\to \exists x\in A\left(\phi \wedge \psi \right)$$