r19.29rOLD

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

		Ref	Expression
	Assertion	r19.29rOLD	$⊢ (\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		ancom	$⊢ (\exists x \in A φ \land \forall x \in A ψ) \leftrightarrow (\forall x \in A ψ \land \exists x \in A φ)$
3		ancom	$⊢ (φ \land ψ) \leftrightarrow (ψ \land φ)$
4	3	rexbii	$⊢ \exists x \in A (φ \land ψ) \leftrightarrow \exists x \in A (ψ \land φ)$
5	1 2 4	3imtr4i	$⊢ (\exists x \in A φ \land \forall x \in A ψ) \to \exists x \in A (φ \land ψ)$

Metamath Proof Explorer

Theorem r19.29rOLD

Proof