Metamath Proof Explorer

Theorem 4exdistr

Description: Distribution of existential quantifiers in a quadruple conjunction. (Contributed by NM, 9-Mar-1995) (Proof shortened by Wolf Lammen, 20-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		19.42v	$⊢ \exists w (χ \land θ) \leftrightarrow (χ \land \exists w θ)$
2	1	anbi2i	$⊢ ((φ \land ψ) \land \exists w (χ \land θ)) \leftrightarrow ((φ \land ψ) \land (χ \land \exists w θ))$
3		19.42v	$⊢ \exists w ((φ \land ψ) \land (χ \land θ)) \leftrightarrow ((φ \land ψ) \land \exists w (χ \land θ))$
4		df-3an	$⊢ (φ \land ψ \land (χ \land \exists w θ)) \leftrightarrow ((φ \land ψ) \land (χ \land \exists w θ))$
5	2 3 4	3bitr4i	$⊢ \exists w ((φ \land ψ) \land (χ \land θ)) \leftrightarrow (φ \land ψ \land (χ \land \exists w θ))$
6	5	3exbii	$⊢ \exists x \exists y \exists z \exists w ((φ \land ψ) \land (χ \land θ)) \leftrightarrow \exists x \exists y \exists z (φ \land ψ \land (χ \land \exists w θ))$
7		3exdistr	$⊢ \exists x \exists y \exists z (φ \land ψ \land (χ \land \exists w θ)) \leftrightarrow \exists x (φ \land \exists y (ψ \land \exists z (χ \land \exists w θ)))$
8	6 7	bitri	$⊢ \exists x \exists y \exists z \exists w ((φ \land ψ) \land (χ \land θ)) \leftrightarrow \exists x (φ \land \exists y (ψ \land \exists z (χ \land \exists w θ)))$