pm11.6

		Ref	Expression
	Assertion	pm11.6	$⊢ \exists x (\exists y (φ \land ψ) \land χ) \leftrightarrow \exists y (\exists x (φ \land χ) \land ψ)$

Step	Hyp	Ref	Expression
1		excom	$⊢ \exists x \exists y ((φ \land ψ) \land χ) \leftrightarrow \exists y \exists x ((φ \land ψ) \land χ)$
2		an32	$⊢ ((φ \land ψ) \land χ) \leftrightarrow ((φ \land χ) \land ψ)$
3	2	2exbii	$⊢ \exists y \exists x ((φ \land ψ) \land χ) \leftrightarrow \exists y \exists x ((φ \land χ) \land ψ)$
4	1 3	bitri	$⊢ \exists x \exists y ((φ \land ψ) \land χ) \leftrightarrow \exists y \exists x ((φ \land χ) \land ψ)$
5		19.41v	$⊢ \exists y ((φ \land ψ) \land χ) \leftrightarrow (\exists y (φ \land ψ) \land χ)$
6	5	exbii	$⊢ \exists x \exists y ((φ \land ψ) \land χ) \leftrightarrow \exists x (\exists y (φ \land ψ) \land χ)$
7		19.41v	$⊢ \exists x ((φ \land χ) \land ψ) \leftrightarrow (\exists x (φ \land χ) \land ψ)$
8	7	exbii	$⊢ \exists y \exists x ((φ \land χ) \land ψ) \leftrightarrow \exists y (\exists x (φ \land χ) \land ψ)$
9	4 6 8	3bitr3i	$⊢ \exists x (\exists y (φ \land ψ) \land χ) \leftrightarrow \exists y (\exists x (φ \land χ) \land ψ)$

Metamath Proof Explorer