sepnsepolem1

		Ref	Expression
	Assertion	sepnsepolem1	$⊢ \exists x \in J \exists y \in J (φ \land ψ \land χ) \leftrightarrow \exists x \in J (φ \land \exists y \in J (ψ \land χ))$

Step	Hyp	Ref	Expression
1		3anass	$⊢ (φ \land ψ \land χ) \leftrightarrow (φ \land (ψ \land χ))$
2	1	2rexbii	$⊢ \exists x \in J \exists y \in J (φ \land ψ \land χ) \leftrightarrow \exists x \in J \exists y \in J (φ \land (ψ \land χ))$
3		r19.42v	$⊢ \exists y \in J (φ \land (ψ \land χ)) \leftrightarrow (φ \land \exists y \in J (ψ \land χ))$
4	3	rexbii	$⊢ \exists x \in J \exists y \in J (φ \land (ψ \land χ)) \leftrightarrow \exists x \in J (φ \land \exists y \in J (ψ \land χ))$
5	2 4	bitri	$⊢ \exists x \in J \exists y \in J (φ \land ψ \land χ) \leftrightarrow \exists x \in J (φ \land \exists y \in J (ψ \land χ))$

Metamath Proof Explorer