This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	1 2	bianbi	$⊢ \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		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
5	4	2rexbii	$⊢ \exists y \in B \exists z \in C (φ \land ψ \land χ) \leftrightarrow \exists y \in B \exists z \in C ((φ \land ψ) \land χ)$
6		reeanv	$⊢ \exists y \in B \exists z \in C ((φ \land ψ) \land χ) \leftrightarrow (\exists y \in B (φ \land ψ) \land \exists z \in C χ)$
7	5 6	bitri	$⊢ \exists y \in B \exists z \in C (φ \land ψ \land χ) \leftrightarrow (\exists y \in B (φ \land ψ) \land \exists z \in C χ)$
8	7	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 χ)$
9		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 χ)$
10	3 8 9	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 χ)$