19.41v

Description: Version of 19.41 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)

		Ref	Expression
	Assertion	19.41v	$⊢ \exists x (φ \land ψ) \leftrightarrow (\exists x φ \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		19.40	$⊢ \exists x (φ \land ψ) \to (\exists x φ \land \exists x ψ)$
2		ax5e	$⊢ \exists x ψ \to ψ$
3	2	anim2i	$⊢ (\exists x φ \land \exists x ψ) \to (\exists x φ \land ψ)$
4	1 3	syl	$⊢ \exists x (φ \land ψ) \to (\exists x φ \land ψ)$
5		pm3.21	$⊢ ψ \to (φ \to (φ \land ψ))$
6	5	eximdv	$⊢ ψ \to (\exists x φ \to \exists x (φ \land ψ))$
7	6	impcom	$⊢ (\exists x φ \land ψ) \to \exists x (φ \land ψ)$
8	4 7	impbii	$⊢ \exists x (φ \land ψ) \leftrightarrow (\exists x φ \land ψ)$

Metamath Proof Explorer

Theorem 19.41v

Proof