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

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

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