Metamath Proof Explorer

Theorem 3reeanv

Description: Rearrange three restricted existential quantifiers. (Contributed by Jeff Madsen, 11-Jun-2010)

		Ref	Expression
	Assertion	3reeanv	$⊢ \exists x \in A \exists y \in B \exists z \in C (φ \land ψ \land χ) \leftrightarrow (\exists x \in A φ \land \exists y \in B ψ \land \exists z \in C χ)$

Proof

Step	Hyp	Ref	Expression
1		r19.41v	$⊢ \exists x \in A (\exists y \in B (φ \land ψ) \land \exists z \in C χ) \leftrightarrow (\exists x \in A \exists y \in B (φ \land ψ) \land \exists z \in C χ)$
2		reeanv	$⊢ \exists x \in A \exists y \in B (φ \land ψ) \leftrightarrow (\exists x \in A φ \land \exists y \in B ψ)$
3	2	anbi1i	$⊢ (\exists x \in A \exists y \in B (φ \land ψ) \land \exists z \in C χ) \leftrightarrow ((\exists x \in A φ \land \exists y \in B ψ) \land \exists z \in C χ)$
4	1 3	bitri	$⊢ \exists x \in A (\exists y \in B (φ \land ψ) \land \exists z \in C χ) \leftrightarrow ((\exists x \in A φ \land \exists y \in B ψ) \land \exists z \in C χ)$
5		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
6	5	2rexbii	$⊢ \exists y \in B \exists z \in C (φ \land ψ \land χ) \leftrightarrow \exists y \in B \exists z \in C ((φ \land ψ) \land χ)$
7		reeanv	$⊢ \exists y \in B \exists z \in C ((φ \land ψ) \land χ) \leftrightarrow (\exists y \in B (φ \land ψ) \land \exists z \in C χ)$
8	6 7	bitri	$⊢ \exists y \in B \exists z \in C (φ \land ψ \land χ) \leftrightarrow (\exists y \in B (φ \land ψ) \land \exists z \in C χ)$
9	8	rexbii	$⊢ \exists x \in A \exists y \in B \exists z \in C (φ \land ψ \land χ) \leftrightarrow \exists x \in A (\exists y \in B (φ \land ψ) \land \exists z \in C χ)$
10		df-3an	$⊢ (\exists x \in A φ \land \exists y \in B ψ \land \exists z \in C χ) \leftrightarrow ((\exists x \in A φ \land \exists y \in B ψ) \land \exists z \in C χ)$
11	4 9 10	3bitr4i	$⊢ \exists x \in A \exists y \in B \exists z \in C (φ \land ψ \land χ) \leftrightarrow (\exists x \in A φ \land \exists y \in B ψ \land \exists z \in C χ)$