Metamath Proof Explorer

Theorem 3exdistr

Description: Distribution of existential quantifiers in a triple conjunction. (Contributed by NM, 9-Mar-1995) (Proof shortened by Andrew Salmon, 25-May-2011)

		Ref	Expression
	Assertion	3exdistr	$⊢ \exists x \exists y \exists z (φ \land ψ \land χ) \leftrightarrow \exists x (φ \land \exists y (ψ \land \exists z χ))$

Proof

Step	Hyp	Ref	Expression
1		3anass	$⊢ (φ \land ψ \land χ) \leftrightarrow (φ \land (ψ \land χ))$
2	1	2exbii	$⊢ \exists y \exists z (φ \land ψ \land χ) \leftrightarrow \exists y \exists z (φ \land (ψ \land χ))$
3		19.42vv	$⊢ \exists y \exists z (φ \land (ψ \land χ)) \leftrightarrow (φ \land \exists y \exists z (ψ \land χ))$
4		exdistr	$⊢ \exists y \exists z (ψ \land χ) \leftrightarrow \exists y (ψ \land \exists z χ)$
5	4	anbi2i	$⊢ (φ \land \exists y \exists z (ψ \land χ)) \leftrightarrow (φ \land \exists y (ψ \land \exists z χ))$
6	2 3 5	3bitri	$⊢ \exists y \exists z (φ \land ψ \land χ) \leftrightarrow (φ \land \exists y (ψ \land \exists z χ))$
7	6	exbii	$⊢ \exists x \exists y \exists z (φ \land ψ \land χ) \leftrightarrow \exists x (φ \land \exists y (ψ \land \exists z χ))$