mopick2

Description: "At most one" can show the existence of a common value. In this case we can infer existence of conjunction from a conjunction of existence, and it is one way to achieve the converse of 19.40 . (Contributed by NM, 5-Apr-2004) (Proof shortened by Andrew Salmon, 9-Jul-2011)

		Ref	Expression
	Assertion	mopick2	$⊢ (\exists^{*} x φ \land \exists x (φ \land ψ) \land \exists x (φ \land χ)) \to \exists x (φ \land ψ \land χ)$

Proof

Step	Hyp	Ref	Expression
1		nfmo1	$⊢ Ⅎ x \exists^{*} x φ$
2		nfe1	$⊢ Ⅎ x \exists x (φ \land ψ)$
3	1 2	nfan	$⊢ Ⅎ x (\exists^{*} x φ \land \exists x (φ \land ψ))$
4		mopick	$⊢ (\exists^{*} x φ \land \exists x (φ \land ψ)) \to (φ \to ψ)$
5	4	ancld	$⊢ (\exists^{*} x φ \land \exists x (φ \land ψ)) \to (φ \to (φ \land ψ))$
6	5	anim1d	$⊢ (\exists^{*} x φ \land \exists x (φ \land ψ)) \to ((φ \land χ) \to ((φ \land ψ) \land χ))$
7		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
8	6 7	imbitrrdi	$⊢ (\exists^{*} x φ \land \exists x (φ \land ψ)) \to ((φ \land χ) \to (φ \land ψ \land χ))$
9	3 8	eximd	$⊢ (\exists^{*} x φ \land \exists x (φ \land ψ)) \to (\exists x (φ \land χ) \to \exists x (φ \land ψ \land χ))$
10	9	3impia	$⊢ (\exists^{*} x φ \land \exists x (φ \land ψ) \land \exists x (φ \land χ)) \to \exists x (φ \land ψ \land χ)$

Metamath Proof Explorer

Theorem mopick2

Proof