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	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 ( 𝜓 ∧ ∃ 𝑧 ( 𝜒 ∧ ∃ 𝑤 𝜃 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		19.42v	⊢ ( ∃ 𝑤 ( 𝜒 ∧ 𝜃 ) ↔ ( 𝜒 ∧ ∃ 𝑤 𝜃 ) )
2	1	anbi2i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑤 ( 𝜒 ∧ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ ∃ 𝑤 𝜃 ) ) )
3		19.42v	⊢ ( ∃ 𝑤 ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑤 ( 𝜒 ∧ 𝜃 ) ) )
4		df-3an	⊢ ( ( 𝜑 ∧ 𝜓 ∧ ( 𝜒 ∧ ∃ 𝑤 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ ∃ 𝑤 𝜃 ) ) )
5	2 3 4	3bitr4i	⊢ ( ∃ 𝑤 ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( 𝜑 ∧ 𝜓 ∧ ( 𝜒 ∧ ∃ 𝑤 𝜃 ) ) )
6	5	3exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝜑 ∧ 𝜓 ∧ ( 𝜒 ∧ ∃ 𝑤 𝜃 ) ) )
7		3exdistr	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝜑 ∧ 𝜓 ∧ ( 𝜒 ∧ ∃ 𝑤 𝜃 ) ) ↔ ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 ( 𝜓 ∧ ∃ 𝑧 ( 𝜒 ∧ ∃ 𝑤 𝜃 ) ) ) )
8	6 7	bitri	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 ( 𝜓 ∧ ∃ 𝑧 ( 𝜒 ∧ ∃ 𝑤 𝜃 ) ) ) )